Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:470 to 483

Mathematical statement

Exact Lean statement

lemma aestronglyMeasurable_ennreal_toReal_iff {f : α → ℝ≥0∞}
    (hf : NullMeasurableSet (f ⁻¹' {∞}) μ) :
    AEStronglyMeasurable (ENNReal.toReal ∘ f) μ ↔ AEStronglyMeasurable f μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma aestronglyMeasurable_ennreal_toReal_iff {f : α → ℝ≥0∞}    (hf : NullMeasurableSet (f ⁻¹' {∞}) μ) :    AEStronglyMeasurable (ENNReal.toReal ∘ f) μ ↔ AEStronglyMeasurable f μ := by  refine ⟨fun h ↦ AEMeasurable.aestronglyMeasurable (NullMeasurable.aemeasurable fun s hs ↦ ?_),    fun h ↦ h.ennreal_toReal⟩  have := h.aemeasurable.nullMeasurable (hs.preimage measurable_ofReal)  simp_rw [preimage_comp] at this  rw [toReal_ofReal_preimage (s := s)]  split_ifs  · exact this  · simp_rw [preimage_sdiff]    exact this.diff hf  · simp_rw [preimage_union]    exact this.union hf