exists_set_sigmaFinite — Mathlib

English

If f is AEFinStronglyMeasurable, then there exists a measurable set t such that f = 0 a.e. on tᶜ and μ|t is sigma-finite.

Русский

Если f — AEFinStronglyMeasurable, тогда существует измеримое множество t такое, что f = 0 почти всюду на комплемента t и μ|t сигма-конечна.

LaTeX

$$$\\exists t\\,\\bigl(\\text{MeasurableSet}(t) \\land f =^{\\mathrm{a}}_{\\mu|_{t^c}} 0 \\land \\Sigma\\text{-finite}(\\mu|_t)\\bigr)$$$

Lean4

theorem exists_set_sigmaFinite (hf : AEFinStronglyMeasurable f μ) :
    ∃ t, MeasurableSet t ∧ f =ᵐ[μ.restrict tᶜ] 0 ∧ SigmaFinite (μ.restrict t) :=
  by
  rcases hf with ⟨g, hg, hfg⟩
  obtain ⟨t, ht, hgt_zero, htμ⟩ := hg.exists_set_sigmaFinite
  refine ⟨t, ht, ?_, htμ⟩
  refine EventuallyEq.trans (ae_restrict_of_ae hfg) ?_
  rw [EventuallyEq, ae_restrict_iff' ht.compl]
  exact Eventually.of_forall hgt_zero

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