From 95abf566ab8589bba96a224cedc7cc40575f869a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Sat, 9 Mar 2024 08:55:53 +0000 Subject: [PATCH] feat: `tendsto_of_integral_tendsto_of_monotone` (#11167) Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`. Also: - move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue. - add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`. Co-authored-by: sgouezel --- .../Constructions/BorelSpace/Basic.lean | 81 +++++++++ .../Constructions/BorelSpace/Metrizable.lean | 40 +---- .../Function/AEMeasurableSequence.lean | 4 + Mathlib/MeasureTheory/Integral/Bochner.lean | 83 ++++++++++ Mathlib/MeasureTheory/Integral/Lebesgue.lean | 154 ++++++++++++++++++ scripts/style-exceptions.txt | 2 +- 6 files changed, 325 insertions(+), 39 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index 4df11a4a085e1..74e8a0ae271e2 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -2162,6 +2162,61 @@ instance : MeasurableSMul ℝ≥0 ℝ≥0∞ where simp_rw [ENNReal.smul_def] exact measurable_coe_nnreal_ennreal.mul_const _ +/-- A limit (over a general filter) of measurable `ℝ≥0∞` valued functions is measurable. -/ +theorem measurable_of_tendsto' {ι : Type*} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞} (u : Filter ι) + [NeBot u] [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) : + Measurable g := by + rcases u.exists_seq_tendsto with ⟨x, hx⟩ + rw [tendsto_pi_nhds] at lim + have : (fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop) = g := by + ext1 y + exact ((lim y).comp hx).liminf_eq + rw [← this] + show Measurable fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop + exact measurable_liminf fun n => hf (x n) +#align measurable_of_tendsto_ennreal' ENNReal.measurable_of_tendsto' + +-- 2024-03-09 +@[deprecated] alias _root_.measurable_of_tendsto_ennreal' := ENNReal.measurable_of_tendsto' + +/-- A sequential limit of measurable `ℝ≥0∞` valued functions is measurable. -/ +theorem measurable_of_tendsto {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞} (hf : ∀ i, Measurable (f i)) + (lim : Tendsto f atTop (𝓝 g)) : Measurable g := + measurable_of_tendsto' atTop hf lim +#align measurable_of_tendsto_ennreal ENNReal.measurable_of_tendsto + +-- 2024-03-09 +@[deprecated] alias _root_.measurable_of_tendsto_ennreal := ENNReal.measurable_of_tendsto + +/-- A limit (over a general filter) of a.e.-measurable `ℝ≥0∞` valued functions is +a.e.-measurable. -/ +lemma aemeasurable_of_tendsto' {ι : Type*} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞} + {μ : Measure α} (u : Filter ι) [NeBot u] [IsCountablyGenerated u] + (hf : ∀ i, AEMeasurable (f i) μ) (hlim : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))) : + AEMeasurable g μ := by + rcases u.exists_seq_tendsto with ⟨v, hv⟩ + have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n ↦ hf (v n) + set p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Tendsto f' atTop (𝓝 (g x)) + have hp : ∀ᵐ x ∂μ, p x fun n ↦ f (v n) x := by + filter_upwards [hlim] with x hx using hx.comp hv + set aeSeqLim := fun x ↦ ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some + refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p) + (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩ + · unfold_let aeSeqLim + simp_rw [aeSeq] + split_ifs with hx + · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx] + exact aeSeq.fun_prop_of_mem_aeSeqSet h'f hx + · exact tendsto_const_nhds + · exact (ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some) + (aeSeqSet h'f p) (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm + +/-- A limit of a.e.-measurable `ℝ≥0∞` valued functions is a.e.-measurable. -/ +lemma aemeasurable_of_tendsto {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞} {μ : Measure α} + (hf : ∀ i, AEMeasurable (f i) μ) (hlim : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (g a))) : + AEMeasurable g μ := + aemeasurable_of_tendsto' atTop hf hlim + end ENNReal @[measurability] @@ -2301,6 +2356,32 @@ theorem AEMeasurable.coe_ereal_ennreal {f : α → ℝ≥0∞} {μ : Measure α} measurable_coe_ennreal_ereal.comp_aemeasurable hf #align ae_measurable.coe_ereal_ennreal AEMeasurable.coe_ereal_ennreal +namespace NNReal + +/-- A limit (over a general filter) of measurable `ℝ≥0` valued functions is measurable. -/ +theorem measurable_of_tendsto' {ι} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : Filter ι) [NeBot u] + [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) : + Measurable g := by + simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf ⊢ + refine' ENNReal.measurable_of_tendsto' u hf _ + rw [tendsto_pi_nhds] at lim ⊢ + exact fun x => (ENNReal.continuous_coe.tendsto (g x)).comp (lim x) +#align measurable_of_tendsto_nnreal' NNReal.measurable_of_tendsto' + +-- 2024-03-09 +@[deprecated] alias _root_.measurable_of_tendsto_nnreal' := NNReal.measurable_of_tendsto' + +/-- A sequential limit of measurable `ℝ≥0` valued functions is measurable. -/ +theorem measurable_of_tendsto {f : ℕ → α → ℝ≥0} {g : α → ℝ≥0} (hf : ∀ i, Measurable (f i)) + (lim : Tendsto f atTop (𝓝 g)) : Measurable g := + measurable_of_tendsto' atTop hf lim +#align measurable_of_tendsto_nnreal NNReal.measurable_of_tendsto + +-- 2024-03-09 +@[deprecated] alias _root_.measurable_of_tendsto_nnreal := NNReal.measurable_of_tendsto + +end NNReal + /-- If a function `f : α → ℝ≥0` is measurable and the measure is σ-finite, then there exists spanning measurable sets with finite measure on which `f` is bounded. See also `StronglyMeasurable.exists_spanning_measurableSet_norm_le` for functions into normed diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean index 4371d5e2f1480..a80f24f41fdda 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean @@ -26,42 +26,6 @@ variable [TopologicalSpace β] [PseudoMetrizableSpace β] [MeasurableSpace β] [ open Metric -/-- A limit (over a general filter) of measurable `ℝ≥0∞` valued functions is measurable. -/ -theorem measurable_of_tendsto_ennreal' {ι} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞} (u : Filter ι) - [NeBot u] [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) : - Measurable g := by - rcases u.exists_seq_tendsto with ⟨x, hx⟩ - rw [tendsto_pi_nhds] at lim - have : (fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop) = g := by - ext1 y - exact ((lim y).comp hx).liminf_eq - rw [← this] - show Measurable fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop - exact measurable_liminf fun n => hf (x n) -#align measurable_of_tendsto_ennreal' measurable_of_tendsto_ennreal' - -/-- A sequential limit of measurable `ℝ≥0∞` valued functions is measurable. -/ -theorem measurable_of_tendsto_ennreal {f : ℕ → α → ℝ≥0∞} {g : α → ℝ≥0∞} (hf : ∀ i, Measurable (f i)) - (lim : Tendsto f atTop (𝓝 g)) : Measurable g := - measurable_of_tendsto_ennreal' atTop hf lim -#align measurable_of_tendsto_ennreal measurable_of_tendsto_ennreal - -/-- A limit (over a general filter) of measurable `ℝ≥0` valued functions is measurable. -/ -theorem measurable_of_tendsto_nnreal' {ι} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : Filter ι) [NeBot u] - [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) : - Measurable g := by - simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf ⊢ - refine' measurable_of_tendsto_ennreal' u hf _ - rw [tendsto_pi_nhds] at lim ⊢ - exact fun x => (ENNReal.continuous_coe.tendsto (g x)).comp (lim x) -#align measurable_of_tendsto_nnreal' measurable_of_tendsto_nnreal' - -/-- A sequential limit of measurable `ℝ≥0` valued functions is measurable. -/ -theorem measurable_of_tendsto_nnreal {f : ℕ → α → ℝ≥0} {g : α → ℝ≥0} (hf : ∀ i, Measurable (f i)) - (lim : Tendsto f atTop (𝓝 g)) : Measurable g := - measurable_of_tendsto_nnreal' atTop hf lim -#align measurable_of_tendsto_nnreal measurable_of_tendsto_nnreal - /-- A limit (over a general filter) of measurable functions valued in a (pseudo) metrizable space is measurable. -/ theorem measurable_of_tendsto_metrizable' {ι} {f : ι → α → β} {g : α → β} (u : Filter ι) [NeBot u] @@ -72,7 +36,7 @@ theorem measurable_of_tendsto_metrizable' {ι} {f : ι → α → β} {g : α intro s h1s h2s h3s have : Measurable fun x => infNndist (g x) s := by suffices Tendsto (fun i x => infNndist (f i x) s) u (𝓝 fun x => infNndist (g x) s) from - measurable_of_tendsto_nnreal' u (fun i => (hf i).infNndist) this + NNReal.measurable_of_tendsto' u (fun i => (hf i).infNndist) this rw [tendsto_pi_nhds] at lim ⊢ intro x exact ((continuous_infNndist_pt s).tendsto (g x)).comp (lim x) @@ -185,7 +149,7 @@ lemma measurableSet_of_tendsto_indicator [NeBot L] (As_mble : ∀ i, MeasurableS (h_lim : ∀ x, ∀ᶠ i in L, x ∈ As i ↔ x ∈ A) : MeasurableSet A := by simp_rw [← measurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢ - exact measurable_of_tendsto_ennreal' L As_mble + exact ENNReal.measurable_of_tendsto' L As_mble ((tendsto_indicator_const_iff_forall_eventually L (1 : ℝ≥0∞)).mpr h_lim) /-- If the indicator functions of a.e.-measurable sets `Aᵢ` converge a.e. to the indicator function diff --git a/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean b/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean index 1f5b550b9cbce..c9705ed264ed2 100644 --- a/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean +++ b/Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean @@ -137,4 +137,8 @@ theorem iSup [CompleteLattice β] [Countable ι] (hf : ∀ i, AEMeasurable (f i) exact measure_mono_null (Set.compl_subset_compl.mpr h_ss) (measure_compl_aeSeqSet_eq_zero hf hp) #align ae_seq.supr aeSeq.iSup +theorem iInf [CompleteLattice β] [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ) + (hp : ∀ᵐ x ∂μ, p x fun n ↦ f n x) : ⨅ n, aeSeq hf p n =ᵐ[μ] ⨅ n, f n := + iSup (β := βᵒᵈ) hf hp + end aeSeq diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean index 82c374761d0de..afa2321640401 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner.lean @@ -1328,6 +1328,89 @@ lemma integral_tendsto_of_tendsto_of_antitone {μ : Measure α} {f : ℕ → α · filter_upwards [h_mono] with x hx n m hnm using neg_le_neg_iff.mpr <| hx hnm · filter_upwards [h_tendsto] with x hx using hx.neg +/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these +functions tends to the integral of the upper bound, then the sequence of functions converges +almost everywhere to the upper bound. -/ +lemma tendsto_of_integral_tendsto_of_monotone {μ : Measure α} {f : ℕ → α → ℝ} {F : α → ℝ} + (hf_int : ∀ n, Integrable (f n) μ) (hF_int : Integrable F μ) + (hf_tendsto : Tendsto (fun i ↦ ∫ a, f i a ∂μ) atTop (𝓝 (∫ a, F a ∂μ))) + (hf_mono : ∀ᵐ a ∂μ, Monotone (fun i ↦ f i a)) + (hf_bound : ∀ᵐ a ∂μ, ∀ i, f i a ≤ F a) : + ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a)) := by + -- reduce to the `ℝ≥0∞` case + let f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a) + let F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a) + have hf'_int_eq : ∀ i, ∫⁻ a, f' i a ∂μ = ENNReal.ofReal (∫ a, f i a ∂μ - ∫ a, f 0 a ∂μ) := by + intro i + unfold_let f' + rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub (hf_int i) (hf_int 0)] + · exact (hf_int i).sub (hf_int 0) + · filter_upwards [hf_mono] with a h_mono + simp [h_mono (zero_le i)] + have hF'_int_eq : ∫⁻ a, F' a ∂μ = ENNReal.ofReal (∫ a, F a ∂μ - ∫ a, f 0 a ∂μ) := by + unfold_let F' + rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub hF_int (hf_int 0)] + · exact hF_int.sub (hf_int 0) + · filter_upwards [hf_bound] with a h_bound + simp [h_bound 0] + have h_tendsto : Tendsto (fun i ↦ ∫⁻ a, f' i a ∂μ) atTop (𝓝 (∫⁻ a, F' a ∂μ)) := by + simp_rw [hf'_int_eq, hF'_int_eq] + refine (ENNReal.continuous_ofReal.tendsto _).comp ?_ + rwa [tendsto_sub_const_iff] + have h_mono : ∀ᵐ a ∂μ, Monotone (fun i ↦ f' i a) := by + filter_upwards [hf_mono] with a ha_mono i j hij + refine ENNReal.ofReal_le_ofReal ?_ + simp [ha_mono hij] + have h_bound : ∀ᵐ a ∂μ, ∀ i, f' i a ≤ F' a := by + filter_upwards [hf_bound] with a ha_bound i + refine ENNReal.ofReal_le_ofReal ?_ + simp only [tsub_le_iff_right, sub_add_cancel, ha_bound i] + -- use the corresponding lemma for `ℝ≥0∞` + have h := tendsto_of_lintegral_tendsto_of_monotone ?_ h_tendsto h_mono h_bound ?_ + rotate_left + · exact (hF_int.1.aemeasurable.sub (hf_int 0).1.aemeasurable).ennreal_ofReal + · exact ((lintegral_ofReal_le_lintegral_nnnorm _).trans_lt (hF_int.sub (hf_int 0)).2).ne + filter_upwards [h, hf_mono, hf_bound] with a ha ha_mono ha_bound + have h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a := by + unfold_let f' + ext i + rw [ENNReal.toReal_ofReal] + · abel + · simp [ha_mono (zero_le i)] + have h2 : F a = (F' a).toReal + f 0 a := by + unfold_let F' + rw [ENNReal.toReal_ofReal] + · abel + · simp [ha_bound 0] + rw [h1, h2] + refine Filter.Tendsto.add ?_ tendsto_const_nhds + exact (ENNReal.continuousAt_toReal ENNReal.ofReal_ne_top).tendsto.comp ha + +/-- If an antitone sequence of functions has a lower bound and the sequence of integrals of these +functions tends to the integral of the lower bound, then the sequence of functions converges +almost everywhere to the lower bound. -/ +lemma tendsto_of_integral_tendsto_of_antitone {μ : Measure α} {f : ℕ → α → ℝ} {F : α → ℝ} + (hf_int : ∀ n, Integrable (f n) μ) (hF_int : Integrable F μ) + (hf_tendsto : Tendsto (fun i ↦ ∫ a, f i a ∂μ) atTop (𝓝 (∫ a, F a ∂μ))) + (hf_mono : ∀ᵐ a ∂μ, Antitone (fun i ↦ f i a)) + (hf_bound : ∀ᵐ a ∂μ, ∀ i, F a ≤ f i a) : + ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a)) := by + let f' : ℕ → α → ℝ := fun i a ↦ - f i a + let F' : α → ℝ := fun a ↦ - F a + suffices ∀ᵐ a ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a)) by + filter_upwards [this] with a ha_tendsto + convert ha_tendsto.neg + · simp [f'] + · simp [F'] + refine tendsto_of_integral_tendsto_of_monotone (fun n ↦ (hf_int n).neg) hF_int.neg ?_ ?_ ?_ + · convert hf_tendsto.neg + · rw [integral_neg] + · rw [integral_neg] + · filter_upwards [hf_mono] with a ha i j hij + simp [f', ha hij] + · filter_upwards [hf_bound] with a ha i + simp [f', F', ha i] + section NormedAddCommGroup variable {H : Type*} [NormedAddCommGroup H] diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue.lean b/Mathlib/MeasureTheory/Integral/Lebesgue.lean index c552f6df12fcf..cee7d140603d1 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue.lean @@ -1052,6 +1052,25 @@ theorem lintegral_iInf {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, Measurab lintegral_iInf_ae h_meas (fun n => ae_of_all _ <| h_anti n.le_succ) h_fin #align measure_theory.lintegral_infi MeasureTheory.lintegral_iInf +theorem lintegral_iInf' {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, AEMeasurable (f n) μ) + (h_anti : ∀ᵐ a ∂μ, Antitone (fun i ↦ f i a)) (h_fin : ∫⁻ a, f 0 a ∂μ ≠ ∞) : + ∫⁻ a, ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ a, f n a ∂μ := by + simp_rw [← iInf_apply] + let p : α → (ℕ → ℝ≥0∞) → Prop := fun _ f' => Antitone f' + have hp : ∀ᵐ x ∂μ, p x fun i => f i x := h_anti + have h_ae_seq_mono : Antitone (aeSeq h_meas p) := by + intro n m hnm x + by_cases hx : x ∈ aeSeqSet h_meas p + · exact aeSeq.prop_of_mem_aeSeqSet h_meas hx hnm + · simp only [aeSeq, hx, if_false] + exact le_rfl + rw [lintegral_congr_ae (aeSeq.iInf h_meas hp).symm] + simp_rw [iInf_apply] + rw [lintegral_iInf (aeSeq.measurable h_meas p) h_ae_seq_mono] + · congr + exact funext fun n ↦ lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp n) + · rwa [lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp 0)] + /-- Monotone convergence for an infimum over a directed family and indexed by a countable type -/ theorem lintegral_iInf_directed_of_measurable {mα : MeasurableSpace α} [Countable β] {f : β → α → ℝ≥0∞} {μ : Measure α} (hμ : μ ≠ 0) (hf : ∀ b, Measurable (f b)) @@ -1198,6 +1217,21 @@ theorem tendsto_lintegral_filter_of_dominated_convergence {ι} {l : Filter ι} assumption #align measure_theory.tendsto_lintegral_filter_of_dominated_convergence MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence +theorem lintegral_tendsto_of_tendsto_of_antitone {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞} + (hf : ∀ n, AEMeasurable (f n) μ) (h_anti : ∀ᵐ x ∂μ, Antitone fun n ↦ f n x) + (h0 : ∫⁻ a, f 0 a ∂μ ≠ ∞) + (h_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))) : + Tendsto (fun n ↦ ∫⁻ x, f n x ∂μ) atTop (𝓝 (∫⁻ x, F x ∂μ)) := by + have : Antitone fun n ↦ ∫⁻ x, f n x ∂μ := fun i j hij ↦ + lintegral_mono_ae (h_anti.mono fun x hx ↦ hx hij) + suffices key : ∫⁻ x, F x ∂μ = ⨅ n, ∫⁻ x, f n x ∂μ by + rw [key] + exact tendsto_atTop_iInf this + rw [← lintegral_iInf' hf h_anti h0] + refine lintegral_congr_ae ?_ + filter_upwards [h_anti, h_tendsto] with _ hx_anti hx_tendsto + using tendsto_nhds_unique hx_tendsto (tendsto_atTop_iInf hx_anti) + section open Encodable @@ -1641,6 +1675,126 @@ theorem _root_.IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal {α : Type exact ENNReal.mul_lt_top ENNReal.coe_lt_top.ne μ_fin.measure_univ_lt_top.ne #align is_finite_measure.lintegral_lt_top_of_bounded_to_ennreal IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal +/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these +functions tends to the integral of the upper bound, then the sequence of functions converges +almost everywhere to the upper bound. Auxiliary version assuming moreover that the +functions in the sequence are ae measurable. -/ +lemma tendsto_of_lintegral_tendsto_of_monotone_aux {α : Type*} {mα : MeasurableSpace α} + {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞} {μ : Measure α} + (hf_meas : ∀ n, AEMeasurable (f n) μ) (hF_meas : AEMeasurable F μ) + (hf_tendsto : Tendsto (fun i ↦ ∫⁻ a, f i a ∂μ) atTop (𝓝 (∫⁻ a, F a ∂μ))) + (hf_mono : ∀ᵐ a ∂μ, Monotone (fun i ↦ f i a)) + (h_bound : ∀ᵐ a ∂μ, ∀ i, f i a ≤ F a) (h_int_finite : ∫⁻ a, F a ∂μ ≠ ∞) : + ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a)) := by + have h_bound_finite : ∀ᵐ a ∂μ, F a ≠ ∞ := by + filter_upwards [ae_lt_top' hF_meas h_int_finite] with a ha using ha.ne + have h_exists : ∀ᵐ a ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) := by + filter_upwards [h_bound, h_bound_finite, hf_mono] with a h_le h_fin h_mono + have h_tendsto : Tendsto (fun i ↦ f i a) atTop atTop ∨ + ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) := tendsto_of_monotone h_mono + cases' h_tendsto with h_absurd h_tendsto + · rw [tendsto_atTop_atTop_iff_of_monotone h_mono] at h_absurd + obtain ⟨i, hi⟩ := h_absurd (F a + 1) + refine absurd (hi.trans (h_le _)) (not_le.mpr ?_) + exact ENNReal.lt_add_right h_fin one_ne_zero + · exact h_tendsto + classical + let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) + then h.choose else ∞ + have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by + filter_upwards [h_exists] with a ha + simp_rw [F', dif_pos ha] + exact ha.choose_spec + suffices F' =ᵐ[μ] F by + filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto + have hF'_le : F' ≤ᵐ[μ] F := by + filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto + exact le_of_tendsto' h_tendsto (fun m ↦ h_le _) + suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from + ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le + refine tendsto_nhds_unique ?_ hf_tendsto + exact lintegral_tendsto_of_tendsto_of_monotone hf_meas hf_mono hF'_tendsto + +/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these +functions tends to the integral of the upper bound, then the sequence of functions converges +almost everywhere to the upper bound. -/ +lemma tendsto_of_lintegral_tendsto_of_monotone {α : Type*} {mα : MeasurableSpace α} + {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞} {μ : Measure α} + (hF_meas : AEMeasurable F μ) + (hf_tendsto : Tendsto (fun i ↦ ∫⁻ a, f i a ∂μ) atTop (𝓝 (∫⁻ a, F a ∂μ))) + (hf_mono : ∀ᵐ a ∂μ, Monotone (fun i ↦ f i a)) + (h_bound : ∀ᵐ a ∂μ, ∀ i, f i a ≤ F a) (h_int_finite : ∫⁻ a, F a ∂μ ≠ ∞) : + ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a)) := by + have : ∀ n, ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f n ∧ ∫⁻ a, f n a ∂μ = ∫⁻ a, g a ∂μ := + fun n ↦ exists_measurable_le_lintegral_eq _ _ + choose g gmeas gf hg using this + let g' : ℕ → α → ℝ≥0∞ := Nat.rec (g 0) (fun n I x ↦ max (g (n+1) x) (I x)) + have M n : Measurable (g' n) := by + induction n with + | zero => simp [g', gmeas 0] + | succ n ih => exact Measurable.max (gmeas (n+1)) ih + have I : ∀ n x, g n x ≤ g' n x := by + intro n x + cases n with | zero | succ => simp [g'] + have I' : ∀ᵐ x ∂μ, ∀ n, g' n x ≤ f n x := by + filter_upwards [hf_mono] with x hx n + induction n with + | zero => simpa [g'] using gf 0 x + | succ n ih => exact max_le (gf (n+1) x) (ih.trans (hx (Nat.le_succ n))) + have Int_eq n : ∫⁻ x, g' n x ∂μ = ∫⁻ x, f n x ∂μ := by + apply le_antisymm + · apply lintegral_mono_ae + filter_upwards [I'] with x hx using hx n + · rw [hg n] + exact lintegral_mono (I n) + have : ∀ᵐ a ∂μ, Tendsto (fun i ↦ g' i a) atTop (𝓝 (F a)) := by + apply tendsto_of_lintegral_tendsto_of_monotone_aux _ hF_meas _ _ _ h_int_finite + · exact fun n ↦ (M n).aemeasurable + · simp_rw [Int_eq] + exact hf_tendsto + · exact eventually_of_forall (fun x ↦ monotone_nat_of_le_succ (fun n ↦ le_max_right _ _)) + · filter_upwards [h_bound, I'] with x h'x hx n using (hx n).trans (h'x n) + filter_upwards [this, I', h_bound] with x hx h'x h''x + exact tendsto_of_tendsto_of_tendsto_of_le_of_le hx tendsto_const_nhds h'x h''x + +/-- If an antitone sequence of functions has a lower bound and the sequence of integrals of these +functions tends to the integral of the lower bound, then the sequence of functions converges +almost everywhere to the lower bound. -/ +lemma tendsto_of_lintegral_tendsto_of_antitone {α : Type*} {mα : MeasurableSpace α} + {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞} {μ : Measure α} + (hf_meas : ∀ n, AEMeasurable (f n) μ) + (hf_tendsto : Tendsto (fun i ↦ ∫⁻ a, f i a ∂μ) atTop (𝓝 (∫⁻ a, F a ∂μ))) + (hf_mono : ∀ᵐ a ∂μ, Antitone (fun i ↦ f i a)) + (h_bound : ∀ᵐ a ∂μ, ∀ i, F a ≤ f i a) (h0 : ∫⁻ a, f 0 a ∂μ ≠ ∞) : + ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a)) := by + have h_int_finite : ∫⁻ a, F a ∂μ ≠ ∞ := by + refine ((lintegral_mono_ae ?_).trans_lt h0.lt_top).ne + filter_upwards [h_bound] with a ha using ha 0 + have h_exists : ∀ᵐ a ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) := by + filter_upwards [hf_mono] with a h_mono + rcases tendsto_of_antitone h_mono with h | h + · refine ⟨0, h.mono_right ?_⟩ + rw [OrderBot.atBot_eq] + exact pure_le_nhds _ + · exact h + classical + let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) + then h.choose else ∞ + have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by + filter_upwards [h_exists] with a ha + simp_rw [F', dif_pos ha] + exact ha.choose_spec + suffices F' =ᵐ[μ] F by + filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto + have hF'_le : F ≤ᵐ[μ] F' := by + filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto + exact ge_of_tendsto' h_tendsto (fun m ↦ h_le _) + suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ by + refine (ae_eq_of_ae_le_of_lintegral_le hF'_le h_int_finite ?_ this.le).symm + exact ENNReal.aemeasurable_of_tendsto hf_meas hF'_tendsto + refine tendsto_nhds_unique ?_ hf_tendsto + exact lintegral_tendsto_of_tendsto_of_antitone hf_meas hf_mono h0 hF'_tendsto + end Lintegral open MeasureTheory.SimpleFunc diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index ef19618997bd1..d7cc13aff5c5e 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -91,7 +91,7 @@ Mathlib/MeasureTheory/Function/LpSpace.lean : line 1 : ERR_NUM_LIN : 2100 file c Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean : line 1 : ERR_NUM_LIN : 2300 file contains 2148 lines, try to split it up Mathlib/MeasureTheory/Integral/Bochner.lean : line 1 : ERR_NUM_LIN : 2100 file contains 1999 lines, try to split it up Mathlib/MeasureTheory/Integral/FundThmCalculus.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1550 lines, try to split it up -Mathlib/MeasureTheory/Integral/Lebesgue.lean : line 1 : ERR_NUM_LIN : 2000 file contains 1851 lines, try to split it up +Mathlib/MeasureTheory/Integral/Lebesgue.lean : line 1 : ERR_NUM_LIN : 2200 file contains 2041 lines, try to split it up Mathlib/MeasureTheory/Integral/SetToL1.lean : line 1 : ERR_NUM_LIN : 2000 file contains 1817 lines, try to split it up Mathlib/MeasureTheory/MeasurableSpace/Basic.lean : line 1 : ERR_NUM_LIN : 2400 file contains 2250 lines, try to split it up Mathlib/MeasureTheory/Measure/MeasureSpace.lean : line 1 : ERR_NUM_LIN : 2300 file contains 2191 lines, try to split it up