From c22a484c8da1ecdef351758fd5a87fc8600e992f Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Thu, 16 Apr 2026 16:31:49 +0800 Subject: [PATCH] refactor: golf AEEqOfIntegral, AEMeasurableOrder, ConditionalExpectation/Real --- .../Function/AEEqOfIntegral.lean | 23 ++--- .../Function/AEMeasurableOrder.lean | 23 ++--- .../Function/ConditionalExpectation/Real.lean | 90 +++++++------------ 3 files changed, 44 insertions(+), 92 deletions(-) diff --git a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean index 62d845f049e668..002ba891b4f87f 100644 --- a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean +++ b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean @@ -357,27 +357,16 @@ theorem ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim (hm : exact hf_zero _ (hs.inter ht_meas) hμs theorem Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero {f : α → E} (hf : Integrable f μ) - (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 := by - have hf_Lp : MemLp f 1 μ := memLp_one_iff_integrable.mpr hf - let f_Lp := hf_Lp.toLp f - have hf_f_Lp : f =ᵐ[μ] f_Lp := (MemLp.coeFn_toLp hf_Lp).symm - refine hf_f_Lp.trans ?_ - refine Lp.ae_eq_zero_of_forall_setIntegral_eq_zero f_Lp one_ne_zero ENNReal.coe_ne_top ?_ ?_ - · exact fun s _ _ => Integrable.integrableOn (L1.integrable_coeFn _) - · intro s hs hμs - rw [integral_congr_ae (ae_restrict_of_ae hf_f_Lp.symm)] - exact hf_zero s hs hμs + (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 := + hf.aefinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero + (fun _ _ _ => hf.integrableOn) hf_zero theorem Integrable.ae_eq_of_forall_setIntegral_eq (f g : α → E) (hf : Integrable f μ) (hg : Integrable g μ) (hfg : ∀ s : Set α, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ) : - f =ᵐ[μ] g := by - rw [← sub_ae_eq_zero] - have hfg' : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by - intro s hs hμs - rw [integral_sub' hf.integrableOn hg.integrableOn] - exact sub_eq_zero.mpr (hfg s hs hμs) - exact Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero (hf.sub hg) hfg' + f =ᵐ[μ] g := + AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq (fun _ _ _ => hf.integrableOn) + (fun _ _ _ => hg.integrableOn) hfg hf.aefinStronglyMeasurable hg.aefinStronglyMeasurable variable {β : Type*} [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] diff --git a/Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean b/Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean index 3cdb2645007327..8942c48fa04cd0 100644 --- a/Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean +++ b/Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean @@ -73,11 +73,7 @@ theorem MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets {α : Type _ = 0 := by simp only [tsum_zero] have ff' : ∀ᵐ x ∂μ, f x = f' x := by have : ∀ᵐ x ∂μ, x ∉ t := by - have : μ t = 0 := le_antisymm μt bot_le - change μ _ = 0 - convert this - ext y - simp only [mem_setOf_eq, mem_compl_iff, not_notMem] + exact measure_eq_zero_iff_ae_notMem.1 (le_antisymm μt bot_le) filter_upwards [this] with x hx apply (iInf_eq_of_forall_ge_of_forall_gt_exists_lt _ _).symm · intro i @@ -86,18 +82,13 @@ theorem MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets {α : Type · simp only [H, le_top, not_false_iff, piecewise_eq_of_notMem] simp only [H, piecewise_eq_of_mem] contrapose! hx - obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (i : β) (f x) ∩ s := - dense_iff_inter_open.1 s_dense (Ioo i (f x)) isOpen_Ioo (nonempty_Ioo.2 hx) - have A : x ∈ v i r := (huv i r).2.2.2.1 rq - refine mem_iUnion.2 ⟨i, ?_⟩ - refine mem_iUnion.2 ⟨⟨r, ⟨rs, xr⟩⟩, ?_⟩ - exact ⟨H, A⟩ + obtain ⟨r, rs, xr, rq⟩ := s_dense.exists_between hx + exact mem_iUnion₂.2 ⟨i, ⟨⟨r, ⟨rs, xr⟩⟩, H, (huv i r).2.2.2.1 rq⟩⟩ · intro q hq - obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (f x) q ∩ s := - dense_iff_inter_open.1 s_dense (Ioo (f x) q) isOpen_Ioo (nonempty_Ioo.2 hq) - refine ⟨⟨r, rs⟩, ?_⟩ - have A : x ∈ u' r := mem_biInter fun i _ => (huv r i).2.2.1 xr - simp only [A, rq, piecewise_eq_of_mem] + obtain ⟨r, rs, xr, rq⟩ := s_dense.exists_between hq + exact ⟨⟨r, rs⟩, by + simp only [show x ∈ u' r from mem_biInter fun i _ => (huv r i).2.2.1 xr, rq, + piecewise_eq_of_mem]⟩ exact ⟨f', f'_meas, ff'⟩ /-- If a function `f : α → ℝ≥0∞` is such that the level sets `{f < p}` and `{q < f}` have measurable diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean index 975db020f35a9a..ea92903abee83c 100644 --- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean +++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne, Kexing Ying module public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator +import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen public import Mathlib.MeasureTheory.Function.UniformIntegrable public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym @@ -55,8 +56,6 @@ theorem rnDeriv_ae_eq_condExp {hm : m ≤ m0} [hμm : SigmaFinite (μ.trim hm)] exact (SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable · exact (SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable.aestronglyMeasurable --- TODO: the following couple of lemmas should be generalized and proved using Jensen's inequality --- for the conditional expectation (not in mathlib yet) . theorem eLpNorm_one_condExp_le_eLpNorm (f : α → ℝ) : eLpNorm (μ[f | m]) 1 μ ≤ eLpNorm f 1 μ := by by_cases hf : Integrable f μ swap; · rw [condExp_of_not_integrable hf, eLpNorm_zero]; exact zero_le _ @@ -64,52 +63,35 @@ theorem eLpNorm_one_condExp_le_eLpNorm (f : α → ℝ) : eLpNorm (μ[f | m]) 1 swap; · rw [condExp_of_not_le hm, eLpNorm_zero]; exact zero_le _ by_cases hsig : SigmaFinite (μ.trim hm) swap; · rw [condExp_of_not_sigmaFinite hm hsig, eLpNorm_zero]; exact zero_le _ - calc - eLpNorm (μ[f | m]) 1 μ ≤ eLpNorm (μ[(|f|) | m]) 1 μ := by - refine eLpNorm_mono_ae ?_ - filter_upwards [condExp_mono hf hf.abs - (ae_of_all μ (fun x => le_abs_self (f x) : ∀ x, f x ≤ |f x|)), - (condExp_neg ..).symm.le.trans (condExp_mono hf.neg hf.abs - (ae_of_all μ (fun x => neg_le_abs (f x) : ∀ x, -f x ≤ |f x|)))] with x hx₁ hx₂ - exact abs_le_abs hx₁ hx₂ - _ = eLpNorm f 1 μ := by - rw [eLpNorm_one_eq_lintegral_enorm, eLpNorm_one_eq_lintegral_enorm, - ← ENNReal.toReal_eq_toReal_iff' (hasFiniteIntegral_iff_enorm.mp integrable_condExp.2).ne - (hasFiniteIntegral_iff_enorm.mp hf.2).ne, - ← integral_norm_eq_lintegral_enorm - (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable, - ← integral_norm_eq_lintegral_enorm hf.1] - simp_rw [Real.norm_eq_abs] - rw (config := { occs := .pos [2] }) [← integral_condExp hm] - refine integral_congr_ae ?_ - have : 0 ≤ᵐ[μ] μ[(|f|) | m] := by - rw [← condExp_zero] - exact condExp_mono (integrable_zero _ _ _) hf.abs - (ae_of_all μ (fun x => abs_nonneg (f x) : ∀ x, 0 ≤ |f x|)) - filter_upwards [this] with x hx - exact abs_eq_self.2 hx + have hleft : eLpNorm (μ[f | m]) 1 μ ≠ ∞ := by + simpa [eLpNorm_one_eq_lintegral_enorm] using + (hasFiniteIntegral_iff_enorm.mp integrable_condExp.2).ne + have hright : eLpNorm f 1 μ ≠ ∞ := by + simpa [eLpNorm_one_eq_lintegral_enorm] using (hasFiniteIntegral_iff_enorm.mp hf.2).ne + rw [← ENNReal.toReal_le_toReal hleft hright] + rw [eLpNorm_one_eq_lintegral_enorm, eLpNorm_one_eq_lintegral_enorm, + ← integral_norm_eq_lintegral_enorm (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable, + ← integral_norm_eq_lintegral_enorm hf.1] + refine (integral_mono_ae integrable_condExp.norm integrable_condExp norm_condExp_le).trans_eq ?_ + exact integral_condExp (μ := μ) (m := m) (m₀ := m0) (f := fun x ↦ ‖f x‖) hm theorem integral_abs_condExp_le (f : α → ℝ) : ∫ x, |(μ[f | m]) x| ∂μ ≤ ∫ x, |f x| ∂μ := by by_cases hm : m ≤ m0 swap · simp_rw [condExp_of_not_le hm, Pi.zero_apply, abs_zero, integral_zero] positivity + by_cases hsig : SigmaFinite (μ.trim hm) + swap + · simp_rw [condExp_of_not_sigmaFinite hm hsig, Pi.zero_apply, abs_zero, integral_zero] + positivity by_cases hfint : Integrable f μ swap · simp only [condExp_of_not_integrable hfint, Pi.zero_apply, abs_zero, integral_const, smul_eq_mul, mul_zero] positivity - rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae] - · apply ENNReal.toReal_mono <;> simp_rw [← Real.norm_eq_abs, ofReal_norm_eq_enorm] - · exact hfint.2.ne - · rw [← eLpNorm_one_eq_lintegral_enorm, ← eLpNorm_one_eq_lintegral_enorm] - exact eLpNorm_one_condExp_le_eLpNorm _ - · filter_upwards with x using abs_nonneg _ - · simp_rw [← Real.norm_eq_abs] - exact hfint.1.norm - · filter_upwards with x using abs_nonneg _ - · simp_rw [← Real.norm_eq_abs] - exact (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable.norm + simp_rw [← Real.norm_eq_abs] + refine (integral_mono_ae integrable_condExp.norm integrable_condExp norm_condExp_le).trans_eq ?_ + exact integral_condExp (μ := μ) (m := m) (m₀ := m0) (f := fun x ↦ ‖f x‖) hm theorem setIntegral_abs_condExp_le {s : Set α} (hs : MeasurableSet[m] s) (f : α → ℝ) : ∫ x in s, |(μ[f | m]) x| ∂μ ≤ ∫ x in s, |f x| ∂μ := by @@ -143,31 +125,21 @@ theorem ae_bdd_condExp_of_ae_bdd {R : ℝ≥0} {f : α → ℝ} (hbdd : ∀ᵐ x swap · simp_rw [condExp_of_not_le hnm, Pi.zero_apply, abs_zero] exact Eventually.of_forall fun _ => R.coe_nonneg + by_cases hsig : SigmaFinite (μ.trim hnm) + swap + · simp_rw [condExp_of_not_sigmaFinite hnm hsig, Pi.zero_apply, abs_zero] + exact Eventually.of_forall fun _ => R.coe_nonneg by_cases hfint : Integrable f μ swap - · simp_rw [condExp_of_not_integrable hfint] + · simp_rw [condExp_of_not_integrable hfint, Pi.zero_apply, abs_zero] + exact Eventually.of_forall fun _ => R.coe_nonneg + have hmem : ∀ᵐ x ∂μ, f x ∈ Set.Icc (-(R : ℝ)) R := by filter_upwards [hbdd] with x hx - rw [Pi.zero_apply, abs_zero] - exact (abs_nonneg _).trans hx - by_contra h - change μ _ ≠ 0 at h - simp only [← pos_iff_ne_zero, Set.compl_def, Set.mem_setOf_eq, not_le] at h - suffices μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R < μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R by - exact this.ne rfl - refine lt_of_lt_of_le (setIntegral_gt_gt R.coe_nonneg ?_ h.ne') ?_ - · exact integrable_condExp.abs.integrableOn - refine (setIntegral_abs_condExp_le ?_ _).trans ?_ - · simp_rw [← Real.norm_eq_abs] - exact @measurableSet_lt _ _ _ _ _ m _ _ _ _ _ measurable_const - stronglyMeasurable_condExp.norm.measurable - simp only [← smul_eq_mul, ← setIntegral_const] - refine setIntegral_mono_ae hfint.abs.integrableOn ?_ hbdd - refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ - (integrable_condExp.integrableOn : IntegrableOn (μ[f|m]) {x | ↑R < |(μ[f|m]) x|} μ).2⟩ - refine setLIntegral_mono - (stronglyMeasurable_condExp.mono hnm).measurable.nnnorm.coe_nnreal_ennreal fun x hx => ?_ - rw [enorm_eq_nnnorm, enorm_eq_nnnorm, ENNReal.coe_le_coe, Real.nnnorm_of_nonneg R.coe_nonneg] - exact Subtype.mk_le_mk.2 (le_of_lt hx) + exact abs_le.mp hx + refine (Convex.condExp_mem (m := m) (mα := m0) hnm hfint isClosed_Icc + (convex_Icc _ _) hmem).mono ?_ + intro x hx + exact abs_le.mpr hx /-- Given an integrable function `g`, the conditional expectations of `g` with respect to a sequence of sub-σ-algebras is uniformly integrable. -/