ae_toFiniteAux — Mathlib

English

For [SFinite μ], ae μ.toFiniteAux = ae μ; the almost-everywhere properties match between μ and its finite auxiliary version.

Русский

Для [SFinite μ] верно ae μ.toFiniteAux = ae μ; свойства почти всюду совпадают между μ и ее конечной вспомогательной версией.

LaTeX

$$$ \ae_{} μ.toFiniteAux = \ae_{=} μ $$$

Lean4

@[local simp]
theorem ae_toFiniteAux [SFinite μ] : ae μ.toFiniteAux = ae μ :=
  by
  rw [Measure.toFiniteAux]
  split_ifs
  · simp
  · obtain ⟨_, h₁, h₂⟩ := (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec
    exact h₂.ae_le.antisymm h₁.ae_le

Похожие утверждения