From e555f3e01c07efde858b9abb2e5f126c27d12a7f Mon Sep 17 00:00:00 2001 From: sgouezel Date: Thu, 21 May 2026 12:04:16 +0200 Subject: [PATCH 1/4] cherry pick --- .../MeasureTheory/Integral/Bochner/Basic.lean | 202 +++++++----------- .../Integral/DominatedConvergence.lean | 16 +- Mathlib/MeasureTheory/Integral/Prod.lean | 2 +- 3 files changed, 81 insertions(+), 139 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean index f7d635f4f3f771..d2a867451c8e07 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean @@ -187,23 +187,25 @@ variable {f : α → E} {m : MeasurableSpace α} {μ : Measure α} section Basic -variable [hE : CompleteSpace E] - -theorem integral_eq (f : α → E) (hf : Integrable f μ) : ∫ a, f a ∂μ = L1.integral (hf.toL1 f) := by +theorem integral_eq [hE : CompleteSpace E] (f : α → E) (hf : Integrable f μ) : + ∫ a, f a ∂μ = L1.integral (hf.toL1 f) := by simp [integral, hE, hf] theorem integral_eq_setToFun (f : α → E) : ∫ a, f a ∂μ = setToFun μ (weightedSMul μ) (dominatedFinMeasAdditive_weightedSMul μ) f := by - simp only [integral, hE, ↓reduceDIte, L1.integral, setToFun]; rfl + by_cases hE : CompleteSpace E + · simp only [integral, hE, ↓reduceDIte, L1.integral, setToFun] + rfl + · simp [integral, hE, setToFun] -theorem L1.integral_eq_integral (f : α →₁[μ] E) : L1.integral f = ∫ a, f a ∂μ := by +theorem L1.integral_eq_integral [CompleteSpace E] (f : α →₁[μ] E) : + L1.integral f = ∫ a, f a ∂μ := by simp only [integral, L1.integral, integral_eq_setToFun] exact (L1.setToFun_eq_setToL1 (dominatedFinMeasAdditive_weightedSMul μ) f).symm theorem integral_undef {f : α → G} (h : ¬Integrable f μ) : ∫ a, f a ∂μ = 0 := by - by_cases hG : CompleteSpace G - · simp [integral, hG, h] - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact setToFun_undef (dominatedFinMeasAdditive_weightedSMul μ) h theorem Integrable.of_integral_ne_zero {f : α → G} (h : ∫ a, f a ∂μ ≠ 0) : Integrable f μ := Not.imp_symm integral_undef h @@ -216,10 +218,8 @@ variable (α G) @[simp] theorem integral_zero : ∫ _ : α, (0 : G) ∂μ = 0 := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact setToFun_zero (dominatedFinMeasAdditive_weightedSMul μ) - · simp [integral, hG] + simp only [integral_eq_setToFun] + apply setToFun_zero @[simp] theorem integral_zero' : integral μ (0 : α → G) = 0 := @@ -236,10 +236,8 @@ theorem integrable_of_integral_eq_one {f : α → ℝ} (h : ∫ x, f x ∂μ = 1 theorem integral_add {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) : ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact setToFun_add (dominatedFinMeasAdditive_weightedSMul μ) hf hg - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact setToFun_add (dominatedFinMeasAdditive_weightedSMul μ) hf hg theorem integral_add' {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) : ∫ a, (f + g) a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ := @@ -247,29 +245,23 @@ theorem integral_add' {f g : α → G} (hf : Integrable f μ) (hg : Integrable g theorem integral_finsetSum {ι} (s : Finset ι) {f : ι → α → G} (hf : ∀ i ∈ s, Integrable (f i) μ) : ∫ a, ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ a, f i a ∂μ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact setToFun_finsetSum (dominatedFinMeasAdditive_weightedSMul _) s hf - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact setToFun_finsetSum (dominatedFinMeasAdditive_weightedSMul _) s hf @[deprecated (since := "2026-04-08")] alias integral_finset_sum := integral_finsetSum @[integral_simps] theorem integral_neg (f : α → G) : ∫ a, -f a ∂μ = -∫ a, f a ∂μ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact setToFun_neg (dominatedFinMeasAdditive_weightedSMul μ) f - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact setToFun_neg (dominatedFinMeasAdditive_weightedSMul μ) f theorem integral_neg' (f : α → G) : ∫ a, (-f) a ∂μ = -∫ a, f a ∂μ := integral_neg f theorem integral_sub {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) : ∫ a, f a - g a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact setToFun_sub (dominatedFinMeasAdditive_weightedSMul μ) hf hg - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact setToFun_sub (dominatedFinMeasAdditive_weightedSMul μ) hf hg theorem integral_sub' {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) : ∫ a, (f - g) a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ := @@ -282,10 +274,8 @@ statement for more general rings with an *a priori* integrability assumption on @[integral_simps] theorem integral_smul [Module 𝕜 G] [NormSMulClass 𝕜 G] [SMulCommClass ℝ 𝕜 G] (c : 𝕜) (f : α → G) : ∫ a, c • f a ∂μ = c • ∫ a, f a ∂μ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact setToFun_smul (dominatedFinMeasAdditive_weightedSMul μ) weightedSMul_smul c f - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact setToFun_smul (dominatedFinMeasAdditive_weightedSMul μ) weightedSMul_smul c f theorem Integrable.integral_smul {R : Type*} [NormedRing R] [Module R G] [IsBoundedSMul R G] [SMulCommClass ℝ R G] (c : R) @@ -307,10 +297,8 @@ theorem integral_div {L : Type*} [RCLike L] (r : L) (f : α → L) : simpa only [← div_eq_mul_inv] using integral_mul_const r⁻¹ f theorem integral_congr_ae {f g : α → G} (h : f =ᵐ[μ] g) : ∫ a, f a ∂μ = ∫ a, g a ∂μ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact setToFun_congr_ae (dominatedFinMeasAdditive_weightedSMul μ) h - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact setToFun_congr_ae (dominatedFinMeasAdditive_weightedSMul μ) h lemma integral_congr_ae₂ {β : Type*} {_ : MeasurableSpace β} {ν : Measure β} {f g : α → β → G} (h : ∀ᵐ a ∂μ, f a =ᵐ[ν] g a) : @@ -323,10 +311,8 @@ lemma integral_congr_ae₂ {β : Type*} {_ : MeasurableSpace β} {ν : Measure @[simp] theorem L1.integral_of_fun_eq_integral' {f : α → G} (hf : Integrable f μ) : ∫ a, (AEEqFun.mk f hf.aestronglyMeasurable) a ∂μ = ∫ a, f a ∂μ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact setToFun_toL1 (dominatedFinMeasAdditive_weightedSMul μ) hf - · simp [MeasureTheory.integral, hG] + simp only [integral_eq_setToFun] + exact setToFun_toL1 (dominatedFinMeasAdditive_weightedSMul μ) hf theorem L1.integral_of_fun_eq_integral {f : α → G} (hf : Integrable f μ) : ∫ a, (hf.toL1 f) a ∂μ = ∫ a, f a ∂μ := by @@ -334,24 +320,17 @@ theorem L1.integral_of_fun_eq_integral {f : α → G} (hf : Integrable f μ) : @[continuity] theorem continuous_integral : Continuous fun f : α →₁[μ] G => ∫ a, f a ∂μ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact continuous_setToFun (dominatedFinMeasAdditive_weightedSMul μ) - · simp [integral, hG, continuous_const] + simp only [integral_eq_setToFun] + exact continuous_setToFun (dominatedFinMeasAdditive_weightedSMul μ) theorem norm_integral_le_lintegral_norm (f : α → G) : ‖∫ a, f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) := by - by_cases hG : CompleteSpace G - · by_cases hf : Integrable f μ - · rw [integral_eq f hf, ← Integrable.norm_toL1_eq_lintegral_norm f hf] - exact L1.norm_integral_le _ - · rw [integral_undef hf, norm_zero]; exact toReal_nonneg - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact (norm_setToFun_le_toReal _ (by simp)).trans (by simp) theorem enorm_integral_le_lintegral_enorm (f : α → G) : ‖∫ a, f a ∂μ‖ₑ ≤ ∫⁻ a, ‖f a‖ₑ ∂μ := by - simp_rw [← ofReal_norm_eq_enorm] - apply ENNReal.ofReal_le_of_le_toReal - exact norm_integral_le_lintegral_norm f + simp only [integral_eq_setToFun] + exact (enorm_setToFun_le _ (by simp)).trans (by simp) theorem dist_integral_le_lintegral_edist {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) : @@ -396,26 +375,24 @@ theorem Integrable.tendsto_setIntegral_nhds_zero {ι} {f : α → G} (hf : Integ hf.2.tendsto_setIntegral_nhds_zero hs /-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x ∂μ`. -/ -theorem tendsto_integral_of_L1 {ι} (f : α → G) (hfi : Integrable f μ) {F : ι → α → G} {l : Filter ι} - (hFi : ∀ᶠ i in l, Integrable (F i) μ) +theorem tendsto_integral_of_L1 {ι} (f : α → G) (hfi : AEStronglyMeasurable f μ) + {F : ι → α → G} {l : Filter ι} (hFi : ∀ᶠ i in l, Integrable (F i) μ) (hF : Tendsto (fun i => ∫⁻ x, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)) : Tendsto (fun i => ∫ x, F i x ∂μ) l (𝓝 <| ∫ x, f x ∂μ) := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ) - f hfi.aestronglyMeasurable hFi hF - · simp [integral, hG, tendsto_const_nhds] + simp only [integral_eq_setToFun] + exact tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ) f hfi hFi hF /-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x ∂μ`. -/ -lemma tendsto_integral_of_L1' {ι} (f : α → G) (hfi : Integrable f μ) {F : ι → α → G} {l : Filter ι} - (hFi : ∀ᶠ i in l, Integrable (F i) μ) (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)) : +lemma tendsto_integral_of_L1' {ι} (f : α → G) (hfi : AEStronglyMeasurable f μ) + {F : ι → α → G} {l : Filter ι} (hFi : ∀ᶠ i in l, Integrable (F i) μ) + (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)) : Tendsto (fun i ↦ ∫ x, F i x ∂μ) l (𝓝 (∫ x, f x ∂μ)) := by refine tendsto_integral_of_L1 f hfi hFi ?_ simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF exact hF /-- If `F i → f` in `L1`, then `∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ`. -/ -lemma tendsto_setIntegral_of_L1 {ι} (f : α → G) (hfi : Integrable f μ) {F : ι → α → G} +lemma tendsto_setIntegral_of_L1 {ι} (f : α → G) (hfi : AEStronglyMeasurable f μ) {F : ι → α → G} {l : Filter ι} (hFi : ∀ᶠ i in l, Integrable (F i) μ) (hF : Tendsto (fun i ↦ ∫⁻ x, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)) (s : Set α) : @@ -427,10 +404,9 @@ lemma tendsto_setIntegral_of_L1 {ι} (f : α → G) (hfi : Integrable f μ) {F : (fun _ ↦ eLpNorm_mono_measure _ Measure.restrict_le_self) /-- If `F i → f` in `L1`, then `∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ`. -/ -lemma tendsto_setIntegral_of_L1' {ι} (f : α → G) (hfi : Integrable f μ) {F : ι → α → G} - {l : Filter ι} - (hFi : ∀ᶠ i in l, Integrable (F i) μ) (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)) - (s : Set α) : +lemma tendsto_setIntegral_of_L1' {ι} (f : α → G) (hfi : AEStronglyMeasurable f μ) {F : ι → α → G} + {l : Filter ι} (hFi : ∀ᶠ i in l, Integrable (F i) μ) + (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)) (s : Set α) : Tendsto (fun i ↦ ∫ x in s, F i x ∂μ) l (𝓝 (∫ x in s, f x ∂μ)) := by refine tendsto_setIntegral_of_L1 f hfi hFi ?_ s simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF @@ -443,43 +419,35 @@ theorem continuousWithinAt_of_dominated {F : X → α → G} {x₀ : X} {bound : (h_bound : ∀ᶠ x in 𝓝[s] x₀, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, ContinuousWithinAt (fun x => F x a) s x₀) : ContinuousWithinAt (fun x => ∫ a, F x a ∂μ) s x₀ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact continuousWithinAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) - hF_meas h_bound bound_integrable h_cont - · simp [integral, hG, continuousWithinAt_const] + simp only [integral_eq_setToFun] + exact continuousWithinAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) + hF_meas h_bound bound_integrable h_cont theorem continuousAt_of_dominated {F : X → α → G} {x₀ : X} {bound : α → ℝ} (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ) (h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, ContinuousAt (fun x => F x a) x₀) : ContinuousAt (fun x => ∫ a, F x a ∂μ) x₀ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact continuousAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) - hF_meas h_bound bound_integrable h_cont - · simp [integral, hG, continuousAt_const] + simp only [integral_eq_setToFun] + exact continuousAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) + hF_meas h_bound bound_integrable h_cont theorem continuousOn_of_dominated {F : X → α → G} {bound : α → ℝ} {s : Set X} (hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ) (h_bound : ∀ x ∈ s, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, ContinuousOn (fun x => F x a) s) : ContinuousOn (fun x => ∫ a, F x a ∂μ) s := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact continuousOn_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) - hF_meas h_bound bound_integrable h_cont - · simp [integral, hG, continuousOn_const] + simp only [integral_eq_setToFun] + exact continuousOn_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) + hF_meas h_bound bound_integrable h_cont theorem continuous_of_dominated {F : X → α → G} {bound : α → ℝ} (hF_meas : ∀ x, AEStronglyMeasurable (F x) μ) (h_bound : ∀ x, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_cont : ∀ᵐ a ∂μ, Continuous fun x => F x a) : Continuous fun x => ∫ a, F x a ∂μ := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact continuous_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) - hF_meas h_bound bound_integrable h_cont - · simp [integral, hG, continuous_const] + simp only [integral_eq_setToFun] + exact continuous_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ) + hF_meas h_bound bound_integrable h_cont /-- The Bochner integral of a real-valued function `f : α → ℝ` is the difference between the integral of the positive part of `f` and the integral of the negative part of `f`. -/ @@ -545,17 +513,18 @@ theorem ofReal_integral_norm_eq_lintegral_enorm {P : Type*} [NormedAddCommGroup rw [integral_norm_eq_lintegral_enorm hf.aestronglyMeasurable, ENNReal.ofReal_toReal] exact lt_top_iff_ne_top.mp (hasFiniteIntegral_iff_enorm.mpr hf.2) -theorem SimpleFunc.integral_eq_integral (f : α →ₛ E) (hfi : Integrable f μ) : +theorem SimpleFunc.integral_eq_integral [CompleteSpace E] (f : α →ₛ E) (hfi : Integrable f μ) : f.integral μ = ∫ x, f x ∂μ := by rw [MeasureTheory.integral_eq f hfi, ← L1.SimpleFunc.toLp_one_eq_toL1, L1.SimpleFunc.integral_L1_eq_integral, L1.SimpleFunc.integral_eq_integral] exact SimpleFunc.integral_congr hfi (Lp.simpleFunc.toSimpleFunc_toLp _ _).symm -theorem SimpleFunc.integral_eq_sum (f : α →ₛ E) (hfi : Integrable f μ) : +theorem SimpleFunc.integral_eq_sum [CompleteSpace E] (f : α →ₛ E) (hfi : Integrable f μ) : ∫ x, f x ∂μ = ∑ x ∈ f.range, μ.real (f ⁻¹' {x}) • x := by rw [← f.integral_eq_integral hfi, SimpleFunc.integral, ← SimpleFunc.integral_eq]; rfl -theorem tendsto_integral_approxOn_of_measurable [MeasurableSpace E] [BorelSpace E] {f : α → E} +theorem tendsto_integral_approxOn_of_measurable [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] + {f : α → E} {s : Set E} [SeparableSpace s] (hfi : Integrable f μ) (hfm : Measurable f) (hs : ∀ᵐ x ∂μ, f x ∈ closure s) {y₀ : E} (h₀ : y₀ ∈ s) (h₀i : Integrable (fun _ => y₀) μ) : Tendsto (fun n => (SimpleFunc.approxOn f hfm s y₀ h₀ n).integral μ) @@ -565,7 +534,8 @@ theorem tendsto_integral_approxOn_of_measurable [MeasurableSpace E] [BorelSpace exact tendsto_setToFun_approxOn_of_measurable (dominatedFinMeasAdditive_weightedSMul μ) hfi hfm hs h₀ h₀i -theorem tendsto_integral_approxOn_of_measurable_of_range_subset [MeasurableSpace E] [BorelSpace E] +theorem tendsto_integral_approxOn_of_measurable_of_range_subset + [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {f : α → E} (fmeas : Measurable f) (hf : Integrable f μ) (s : Set E) [SeparableSpace s] (hs : range f ∪ {0} ⊆ s) : Tendsto (fun n => (SimpleFunc.approxOn f fmeas s 0 (hs <| by simp) n).integral μ) atTop @@ -992,31 +962,16 @@ variable {ν : Measure α} theorem integral_add_measure {f : α → G} (hμ : Integrable f μ) (hν : Integrable f ν) : ∫ x, f x ∂(μ + ν) = ∫ x, f x ∂μ + ∫ x, f x ∂ν := by - by_cases hG : CompleteSpace G; swap - · simp [integral, hG] - have hfi := hμ.add_measure hν - simp_rw [integral_eq_setToFun] - have hμ_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul μ : Set α → G →L[ℝ] G) 1 := - DominatedFinMeasAdditive.add_measure_right μ ν (dominatedFinMeasAdditive_weightedSMul μ) - zero_le_one - have hν_dfma : DominatedFinMeasAdditive (μ + ν) (weightedSMul ν : Set α → G →L[ℝ] G) 1 := - DominatedFinMeasAdditive.add_measure_left μ ν (dominatedFinMeasAdditive_weightedSMul ν) - zero_le_one - rw [← setToFun_congr_measure_of_add_right hμ_dfma - (dominatedFinMeasAdditive_weightedSMul μ) f hfi, - ← setToFun_congr_measure_of_add_left hν_dfma (dominatedFinMeasAdditive_weightedSMul ν) f hfi] - refine setToFun_add_left' _ _ _ (fun s _ hμνs => ?_) f - rw [Measure.coe_add, Pi.add_apply, add_lt_top] at hμνs - rw [weightedSMul, weightedSMul, weightedSMul, ← add_smul, - measureReal_add_apply hμνs.1.ne hμνs.2.ne] + simp only [integral_eq_setToFun] + apply setToFun_add_left'' (fun s hs h's ↦ ?_) hμ hν le_rfl zero_le_one zero_le_one zero_le_one + simp only [Measure.coe_add, Pi.add_apply, add_lt_top] at h's + simp [weightedSMul, Measure.real, toReal_add, h's.1.ne, h's.2.ne, add_smul] @[simp] theorem integral_zero_measure {m : MeasurableSpace α} (f : α → G) : (∫ x, f x ∂(0 : Measure α)) = 0 := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact setToFun_measure_zero (dominatedFinMeasAdditive_weightedSMul _) rfl - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact setToFun_measure_zero (dominatedFinMeasAdditive_weightedSMul _) rfl @[simp] theorem setIntegral_measure_zero (f : α → G) {μ : Measure α} {s : Set α} (hs : μ s = 0) : @@ -1072,20 +1027,11 @@ theorem integral_map_of_stronglyMeasurable {β} [MeasurableSpace β] {φ : α by_cases hfi : Integrable f (Measure.map φ μ); swap · rw [integral_undef hfi, integral_undef] exact fun hfφ => hfi ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hfφ) - borelize G - have : SeparableSpace (range f ∪ {0} : Set G) := hfm.separableSpace_range_union_singleton - refine tendsto_nhds_unique - (tendsto_integral_approxOn_of_measurable_of_range_subset hfm.measurable hfi _ Subset.rfl) ?_ - convert tendsto_integral_approxOn_of_measurable_of_range_subset (hfm.measurable.comp hφ) - ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).1 hfi) (range f ∪ {0}) - (union_subset_union_left {0} (range_comp_subset_range φ f)) using 1 - ext1 i - simp only [SimpleFunc.integral_eq, hφ, SimpleFunc.measurableSet_preimage, map_measureReal_apply, - ← preimage_comp] - refine (Finset.sum_subset (SimpleFunc.range_comp_subset_range _ hφ) fun y _ hy => ?_).symm - rw [SimpleFunc.mem_range, ← Set.preimage_singleton_eq_empty, SimpleFunc.coe_comp] at hy - rw [hy] - simp + simp only [integral_eq_setToFun] + apply setToFun_of_le_map_of_stronglyMeasurable _ _ + ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).1 hfi) hfm hφ le_rfl + intro s x hs + simp [weightedSMul_apply, map_measureReal_apply, hs, hφ] theorem integral_map {β} [MeasurableSpace β] {φ : α → β} (hφ : AEMeasurable φ μ) {f : β → G} (hfm : AEStronglyMeasurable f (Measure.map φ μ)) : @@ -1327,11 +1273,11 @@ theorem integral_trim (hm : m ≤ m0) {f : β → G} (hf : StronglyMeasurable[m] have hf_seq_eq : ∀ n, ∫ x, f_seq n x ∂μ = ∫ x, f_seq n x ∂μ.trim hm := fun n => integral_trim_simpleFunc hm (f_seq n) (hf_seq_int n) have h_lim_1 : atTop.Tendsto (fun n => ∫ x, f_seq n x ∂μ) (𝓝 (∫ x, f x ∂μ)) := by - refine tendsto_integral_of_L1 f hf_int (Eventually.of_forall hf_seq_int) ?_ + refine tendsto_integral_of_L1 f hf_int.1 (Eventually.of_forall hf_seq_int) ?_ exact SimpleFunc.tendsto_approxOn_range_L1_enorm (hf.mono hm).measurable hf_int have h_lim_2 : atTop.Tendsto (fun n => ∫ x, f_seq n x ∂μ) (𝓝 (∫ x, f x ∂μ.trim hm)) := by simp_rw [hf_seq_eq] - refine @tendsto_integral_of_L1 β G _ _ m (μ.trim hm) _ f (hf_int.trim hm hf) _ _ + refine @tendsto_integral_of_L1 β G _ _ m (μ.trim hm) _ f (hf_int.trim hm hf).1 _ _ (Eventually.of_forall hf_seq_int_m) ?_ exact @SimpleFunc.tendsto_approxOn_range_L1_enorm β G m _ _ _ f _ _ hf.measurable (hf_int.trim hm hf) diff --git a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean index 2515789dde32af..1df05bfe95e215 100644 --- a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean +++ b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean @@ -60,11 +60,9 @@ theorem tendsto_integral_of_dominated_convergence {F : ℕ → α → G} {f : α (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) : Tendsto (fun n => ∫ a, F n a ∂μ) atTop (𝓝 <| ∫ a, f a ∂μ) := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact tendsto_setToFun_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ) - bound F_measurable bound_integrable h_bound h_lim - · simp [integral, hG] + simp only [integral_eq_setToFun] + exact tendsto_setToFun_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ) + bound F_measurable bound_integrable h_bound h_lim /-- Lebesgue dominated convergence theorem for filters with a countable basis -/ theorem tendsto_integral_filter_of_dominated_convergence {ι} {l : Filter ι} [l.IsCountablyGenerated] @@ -72,11 +70,9 @@ theorem tendsto_integral_filter_of_dominated_convergence {ι} {l : Filter ι} [l (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a) (bound_integrable : Integrable bound μ) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))) : Tendsto (fun n => ∫ a, F n a ∂μ) l (𝓝 <| ∫ a, f a ∂μ) := by - by_cases hG : CompleteSpace G - · simp only [integral_eq_setToFun] - exact tendsto_setToFun_filter_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ) - bound hF_meas h_bound bound_integrable h_lim - · simp [integral, hG, tendsto_const_nhds] + simp only [integral_eq_setToFun] + exact tendsto_setToFun_filter_of_dominated_convergence (dominatedFinMeasAdditive_weightedSMul μ) + bound hF_meas h_bound bound_integrable h_lim /-- Lebesgue dominated convergence theorem for series. -/ theorem hasSum_integral_of_dominated_convergence {ι} [Countable ι] {F : ι → α → G} {f : α → G} diff --git a/Mathlib/MeasureTheory/Integral/Prod.lean b/Mathlib/MeasureTheory/Integral/Prod.lean index d30a559f11e351..eecf6fee34a64b 100644 --- a/Mathlib/MeasureTheory/Integral/Prod.lean +++ b/Mathlib/MeasureTheory/Integral/Prod.lean @@ -472,7 +472,7 @@ theorem continuous_integral_integral : Continuous fun f : α × β →₁[μ.prod ν] E => ∫ x, ∫ y, f (x, y) ∂ν ∂μ := by rw [continuous_iff_continuousAt]; intro g refine - tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_prod_left + tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_prod_left.aestronglyMeasurable (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_prod_left) ?_ simp_rw [← lintegral_fn_integral_sub _ (L1.integrable_coeFn _) (L1.integrable_coeFn g)] apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _ From 0a7d931524aba86fcfd6f339764225aee63a6026 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Thu, 21 May 2026 13:09:08 +0200 Subject: [PATCH 2/4] fix --- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean | 4 ++-- Mathlib/Probability/Kernel/Disintegration/Density.lean | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean b/Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean index 6395d12eaccb7b..5bd891a3ef2fa5 100644 --- a/Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean +++ b/Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean @@ -216,7 +216,7 @@ theorem Kernel.continuous_integral_integral : Continuous fun f : β × γ →₁[(κ ⊗ₖ η) a] E => ∫ x, ∫ y, f (x, y) ∂η (a, x) ∂κ a := by rw [continuous_iff_continuousAt]; intro g refine - tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_compProd + tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_compProd.aestronglyMeasurable (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_compProd) ?_ simp_rw [← lintegral_fn_integral_sub (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn g)] apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _ @@ -401,7 +401,7 @@ theorem integral_integral_sub'_comp ⦃f g : γ → E⦄ (hf : Integrable f ((η theorem continuous_integral_integral_comp : Continuous fun f : γ →₁[(η ∘ₖ κ) a] E ↦ ∫ x, ∫ y, f y ∂η x ∂κ a := by refine continuous_iff_continuousAt.2 fun g ↦ ?_ - refine tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_comp + refine tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_comp.aestronglyMeasurable (Eventually.of_forall fun h ↦ (L1.integrable_coeFn h).integral_comp) ?_ simp_rw [← lintegral_fn_integral_sub_comp (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn g)] refine tendsto_of_tendsto_of_tendsto_of_le_of_le diff --git a/Mathlib/Probability/Kernel/Disintegration/Density.lean b/Mathlib/Probability/Kernel/Disintegration/Density.lean index 2f18ebc7c8f1a6..3fe7eaab0b5954 100644 --- a/Mathlib/Probability/Kernel/Disintegration/Density.lean +++ b/Mathlib/Probability/Kernel/Disintegration/Density.lean @@ -499,7 +499,8 @@ lemma tendsto_setIntegral_densityProcess (hκν : fst κ ≤ ν) Tendsto (fun i ↦ ∫ x in A, densityProcess κ ν i a x s ∂(ν a)) atTop (𝓝 (∫ x in A, density κ ν a x s ∂(ν a))) := by refine tendsto_setIntegral_of_L1' (μ := ν a) (fun x ↦ density κ ν a x s) - (integrable_density hκν a hs) (F := fun i x ↦ densityProcess κ ν i a x s) (l := atTop) + (integrable_density hκν a hs).aestronglyMeasurable + (F := fun i x ↦ densityProcess κ ν i a x s) (l := atTop) (Eventually.of_forall (fun n ↦ integrable_densityProcess hκν _ _ hs)) ?_ A refine (tendsto_congr fun n ↦ ?_).mp (tendsto_eLpNorm_one_densityProcess_limitProcess hκν a hs) refine eLpNorm_congr_ae ?_ From a0464373aa40da32fb5726a86a9f7c629a84e970 Mon Sep 17 00:00:00 2001 From: Sebastien Gouezel Date: Fri, 22 May 2026 18:45:59 +0200 Subject: [PATCH 3/4] Update Mathlib/MeasureTheory/Integral/Bochner/Basic.lean Co-authored-by: Anatole Dedecker --- Mathlib/MeasureTheory/Integral/Bochner/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean index d2a867451c8e07..831514c4690b8e 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean @@ -524,8 +524,7 @@ theorem SimpleFunc.integral_eq_sum [CompleteSpace E] (f : α →ₛ E) (hfi : In rw [← f.integral_eq_integral hfi, SimpleFunc.integral, ← SimpleFunc.integral_eq]; rfl theorem tendsto_integral_approxOn_of_measurable [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] - {f : α → E} - {s : Set E} [SeparableSpace s] (hfi : Integrable f μ) (hfm : Measurable f) + {f : α → E} {s : Set E} [SeparableSpace s] (hfi : Integrable f μ) (hfm : Measurable f) (hs : ∀ᵐ x ∂μ, f x ∈ closure s) {y₀ : E} (h₀ : y₀ ∈ s) (h₀i : Integrable (fun _ => y₀) μ) : Tendsto (fun n => (SimpleFunc.approxOn f hfm s y₀ h₀ n).integral μ) atTop (𝓝 <| ∫ x, f x ∂μ) := by From 7a02326321a11cb550039b699d1f40b96789772e Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sat, 23 May 2026 09:41:55 +0200 Subject: [PATCH 4/4] avoid case split --- Mathlib/MeasureTheory/Integral/Bochner/Basic.lean | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean index 831514c4690b8e..0f2d1ab194b4a7 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean @@ -543,7 +543,7 @@ theorem tendsto_integral_approxOn_of_measurable_of_range_subset exact Eventually.of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _))) -- We redeclare `E` here to temporarily avoid --- the `[CompleteSpace E]` and `[NormedSpace ℝ E]` instances. +-- the `[NormedSpace ℝ E]` instance. theorem tendsto_integral_norm_approxOn_sub {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {f : α → E} (fmeas : Measurable f) (hf : Integrable f μ) [SeparableSpace (range f ∪ {0} : Set E)] : @@ -591,11 +591,9 @@ variable [ClosedIciTopology E] /-- The integral of a function which is nonnegative almost everywhere is nonnegative. -/ lemma integral_nonneg_of_ae {f : α → E} (hf : 0 ≤ᵐ[μ] f) : - 0 ≤ ∫ x, f x ∂μ := by - by_cases hE : CompleteSpace E - · exact integral_eq_setToFun f ▸ setToFun_nonneg (dominatedFinMeasAdditive_weightedSMul μ) - (fun s _ _ => weightedSMul_nonneg s) hf - · simp [integral, hE] + 0 ≤ ∫ x, f x ∂μ := + integral_eq_setToFun f ▸ setToFun_nonneg (dominatedFinMeasAdditive_weightedSMul μ) + (fun s _ _ => weightedSMul_nonneg s) hf lemma integral_nonneg {f : α → E} (hf : 0 ≤ f) : 0 ≤ ∫ x, f x ∂μ := @@ -1001,8 +999,6 @@ theorem nndist_integral_add_measure_le_lintegral @[simp] theorem integral_smul_measure (f : α → G) (c : ℝ≥0∞) : ∫ x, f x ∂c • μ = c.toReal • ∫ x, f x ∂μ := by - by_cases hG : CompleteSpace G; swap - · simp [integral, hG] -- First we consider the “degenerate” case `c = ∞` rcases eq_or_ne c ∞ with (rfl | hc) · rw [ENNReal.toReal_top, zero_smul, integral_eq_setToFun, setToFun_top_smul_measure] @@ -1021,8 +1017,6 @@ theorem integral_smul_nnreal_measure (f : α → G) (c : ℝ≥0) : theorem integral_map_of_stronglyMeasurable {β} [MeasurableSpace β] {φ : α → β} (hφ : Measurable φ) {f : β → G} (hfm : StronglyMeasurable f) : ∫ y, f y ∂Measure.map φ μ = ∫ x, f (φ x) ∂μ := by - by_cases hG : CompleteSpace G; swap - · simp [integral, hG] by_cases hfi : Integrable f (Measure.map φ μ); swap · rw [integral_undef hfi, integral_undef] exact fun hfφ => hfi ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hfφ)