feat(MeasureTheory/Function): stronger version of Vitali's convergence theorem (#9163)

Prove a stronger version of Vitali's convergence theorem, which does not require an `IsFiniteMeasure` hypothesis. Instead it uses a new uniform tightness hypothesis. The hypothesis `UnifTight` is implemented closely following the structure of the existing `UnifIntegrable`.



Co-authored-by: igorkhavkine <133780155+igorkhavkine@users.noreply.github.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: 3 people

Mathlib/MeasureTheory/Function/UnifTight.lean

@@ -3,14 +3,17 @@ Copyright (c) 2023 Igor Khavkine. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Igor Khavkine
 -/
-import Mathlib.MeasureTheory.Function.LpSpace
+import Mathlib.MeasureTheory.Function.ConvergenceInMeasure
+import Mathlib.MeasureTheory.Function.L1Space
+import Mathlib.MeasureTheory.Function.UniformIntegrable
 
 /-!
 # Uniform tightness
 
 This file contains the definitions for uniform tightness for a family of Lp functions.
 It is used as a hypothesis to the version of Vitali's convergence theorem for Lp spaces
-that works also for spaces of infinite measure.
+that works also for spaces of infinite measure. This version of Vitali's theorem
+is also proved later in the file.
 
 ## Main definitions
 
@@ -23,6 +26,11 @@ that works also for spaces of infinite measure.
 
 * `MeasureTheory.unifTight_finite`: a finite sequence of Lp functions is uniformly
   tight.
+* `MeasureTheory.tendsto_Lp_of_tendsto_ae`: a sequence of Lp functions which is uniformly
+  integrable and uniformly tight converges in Lp if it converges almost everywhere.
+* `MeasureTheory.tendstoInMeasure_iff_tendsto_Lp`: Vitali convergence theorem:
+  a sequence of Lp functions converges in Lp if and only if it is uniformly integrable,
+  uniformly tight and converges in measure.
 
 ## Tags
 
@@ -70,15 +78,16 @@ theorem unifTight_iff_real {_ : MeasurableSpace α} (f : ι → α → β) (p :
 
 namespace UnifTight
 
-theorem eventually_cofinite_indicator (hf : UnifTight f p μ) {ε : ℝ≥0} (hε : ε ≠ 0) :
+theorem eventually_cofinite_indicator (hf : UnifTight f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
     ∀ᶠ s in μ.cofinite.smallSets, ∀ i, snorm (s.indicator (f i)) p μ ≤ ε := by
-  rcases hf (pos_iff_ne_zero.2 hε) with ⟨s, hμs, hfs⟩
-  refine (eventually_smallSets' ?_).2 ⟨sᶜ, ?_, fun i ↦ hfs i⟩
+  by_cases hε_top : ε = ∞; subst hε_top; simp
+  rcases hf (pos_iff_ne_zero.2 (toNNReal_ne_zero.mpr ⟨hε,hε_top⟩)) with ⟨s, hμs, hfs⟩
+  refine (eventually_smallSets' ?_).2 ⟨sᶜ, ?_, fun i ↦ (coe_toNNReal hε_top) ▸ hfs i⟩
   · intro s t hst ht i
     exact (snorm_mono <| norm_indicator_le_of_subset hst _).trans (ht i)
   · rwa [Measure.compl_mem_cofinite, lt_top_iff_ne_top]
 
-protected theorem exists_measurableSet_indicator (hf : UnifTight f p μ) {ε : ℝ≥0} (hε : ε ≠ 0) :
+protected theorem exists_measurableSet_indicator (hf : UnifTight f p μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
     ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∀ i, snorm (sᶜ.indicator (f i)) p μ ≤ ε :=
   let ⟨s, hμs, hsm, hfs⟩ := (hf.eventually_cofinite_indicator hε).exists_measurable_mem_of_smallSets
   ⟨sᶜ, hsm.compl, hμs, by rwa [compl_compl s]⟩
@@ -92,13 +101,12 @@ protected theorem add (hf : UnifTight f p μ) (hg : UnifTight g p μ)
     refine ⟨∅, (by measurability), fun i ↦ ?_⟩
     simp only [compl_empty, indicator_univ, Pi.add_apply]
     exact (hη (f i) (g i) (hf_meas i) (hg_meas i) le_top le_top).le
-  have nnη_nz := (toNNReal_ne_zero.mpr ⟨hη_pos.ne',hη_top⟩)
   obtain ⟨s, hμs, hsm, hfs, hgs⟩ :
       ∃ s ∈ μ.cofinite, MeasurableSet s ∧
-        (∀ i, snorm (s.indicator (f i)) p μ ≤ η.toNNReal) ∧
-        (∀ i, snorm (s.indicator (g i)) p μ ≤ η.toNNReal) :=
-    ((hf.eventually_cofinite_indicator nnη_nz).and
-      (hg.eventually_cofinite_indicator nnη_nz)).exists_measurable_mem_of_smallSets
+        (∀ i, snorm (s.indicator (f i)) p μ ≤ η) ∧
+        (∀ i, snorm (s.indicator (g i)) p μ ≤ η) :=
+    ((hf.eventually_cofinite_indicator hη_pos.ne').and
+      (hg.eventually_cofinite_indicator hη_pos.ne')).exists_measurable_mem_of_smallSets
   refine ⟨sᶜ, ne_of_lt hμs, fun i ↦ ?_⟩
   have η_cast : ↑η.toNNReal = η := coe_toNNReal hη_top
   calc
@@ -199,4 +207,183 @@ theorem unifTight_finite [Finite ι] (hp_top : p ≠ ∞) {f : ι → α → β}
 
 end UnifTight
 
+section VitaliConvergence
+
+variable {μ : Measure α} {p : ℝ≥0∞} {f : ℕ → α → β} {g : α → β}
+
+/-! Both directions and an iff version of Vitali's convergence theorem on measure spaces
+of not necessarily finite volume. See `Thm III.6.15` of Dunford & Schwartz, Part I (1958). -/
+
+/- We start with the reverse direction. We only need to show that uniform tightness follows
+from convergence in Lp. Mathlib already has the analogous `unifIntegrable_of_tendsto_Lp`
+and `tendstoInMeasure_of_tendsto_snorm`. -/
+
+/-- Intermediate lemma for `unifTight_of_tendsto_Lp`. -/
+private theorem unifTight_of_tendsto_Lp_zero (hp' : p ≠ ∞) (hf : ∀ n, Memℒp (f n) p μ)
+    (hf_tendsto : Tendsto (fun n => snorm (f n) p μ) atTop (𝓝 0)) : UnifTight f p μ := fun ε hε ↦by
+  rw [ENNReal.tendsto_atTop_zero] at hf_tendsto
+  obtain ⟨N, hNε⟩ := hf_tendsto ε (by simpa only [gt_iff_lt, ENNReal.coe_pos])
+  let F : Fin N → α → β := fun n => f n
+  have hF : ∀ n, Memℒp (F n) p μ := fun n => hf n
+  obtain ⟨s, hμs, hFε⟩ := unifTight_fin hp' hF hε
+  refine ⟨s, hμs, fun n => ?_⟩
+  by_cases hn : n < N
+  · exact hFε ⟨n, hn⟩
+  · exact (snorm_indicator_le _).trans (hNε n (not_lt.mp hn))
+
+/-- Convergence in Lp implies uniform tightness. -/
+private theorem unifTight_of_tendsto_Lp (hp' : p ≠ ∞) (hf : ∀ n, Memℒp (f n) p μ)
+    (hg : Memℒp g p μ) (hfg : Tendsto (fun n => snorm (f n - g) p μ) atTop (𝓝 0)) :
+    UnifTight f p μ := by
+  have : f = (fun _ => g) + fun n => f n - g := by ext1 n; simp
+  rw [this]
+  refine UnifTight.add ?_ ?_ (fun _ => hg.aestronglyMeasurable)
+      fun n => (hf n).1.sub hg.aestronglyMeasurable
+  · exact unifTight_const hp' hg
+  · exact unifTight_of_tendsto_Lp_zero hp' (fun n => (hf n).sub hg) hfg
+
+/- Next we deal with the forward direction. The `Memℒp` and `TendstoInMeasure` hypotheses
+are unwrapped and strengthened (by known lemmas) to also have the `StronglyMeasurable`
+and a.e. convergence hypotheses. The bulk of the proof is done under these stronger hypotheses.-/
+
+/-- Bulk of the proof under strengthened hypotheses. Invoked from `tendsto_Lp_of_tendsto_ae`. -/
+private theorem tendsto_Lp_of_tendsto_ae_of_meas (hp : 1 ≤ p) (hp' : p ≠ ∞)
+    {f : ℕ → α → β} {g : α → β} (hf : ∀ n, StronglyMeasurable (f n)) (hg : StronglyMeasurable g)
+    (hg' : Memℒp g p μ) (hui : UnifIntegrable f p μ) (hut : UnifTight f p μ)
+    (hfg : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
+    Tendsto (fun n => snorm (f n - g) p μ) atTop (𝓝 0) := by
+  rw [ENNReal.tendsto_atTop_zero]
+  intro ε hε
+  by_cases hfinε : ε ≠ ∞; swap
+  · rw [not_ne_iff.mp hfinε]; exact ⟨0, fun n _ => le_top⟩
+  by_cases hμ : μ = 0
+  · rw [hμ]; use 0; intro n _; rw [snorm_measure_zero]; exact zero_le ε
+  have hε' : 0 < ε / 3 := ENNReal.div_pos hε.ne' (coe_ne_top)
+  -- use tightness to divide the domain into interior and exterior
+  obtain ⟨Eg, hmEg, hμEg, hgε⟩ := Memℒp.exists_snorm_indicator_compl_lt hp' hg' hε'.ne' --hrε'
+  obtain ⟨Ef, hmEf, hμEf, hfε⟩ := hut.exists_measurableSet_indicator hε'.ne'
+  have hmE := hmEf.union hmEg
+  have hfmE := (measure_union_le Ef Eg).trans_lt (add_lt_top.mpr ⟨hμEf, hμEg⟩)
+  set E : Set α := Ef ∪ Eg
+  -- use uniform integrability to get control on the limit over E
+  have hgE' := Memℒp.restrict E hg'
+  have huiE := hui.restrict  E
+  have hfgE : (∀ᵐ x ∂(μ.restrict E), Tendsto (fun n => f n x) atTop (𝓝 (g x))) :=
+    ae_restrict_of_ae hfg
+  -- `tendsto_Lp_of_tendsto_ae_of_meas` needs to
+  -- synthesize an argument `[IsFiniteMeasure (μ.restrict E)]`.
+  -- It is enough to have in the context a term of `Fact (μ E < ∞)`, which is our `ffmE` below,
+  -- which is automatically fed into `Restrict.isFiniteInstance`.
+  have ffmE : Fact _ := { out := hfmE }
+  have hInner := tendsto_Lp_finite_of_tendsto_ae_of_meas hp hp' hf hg hgE' huiE hfgE
+  rw [ENNReal.tendsto_atTop_zero] at hInner
+  -- get a sufficiently large N for given ε, and consider any n ≥ N
+  obtain ⟨N, hfngε⟩ := hInner (ε / 3) hε'
+  use N; intro n hn
+  -- get interior estimates
+  have hmfngE : AEStronglyMeasurable _ μ := (((hf n).sub hg).indicator hmE).aestronglyMeasurable
+  have hfngEε := calc
+    snorm (E.indicator (f n - g)) p μ
+      = snorm (f n - g) p (μ.restrict E) := snorm_indicator_eq_snorm_restrict hmE
+    _ ≤ ε / 3                            := hfngε n hn
+  -- get exterior estimates
+  have hmgEc : AEStronglyMeasurable _ μ := (hg.indicator hmE.compl).aestronglyMeasurable
+  have hgEcε := calc
+    snorm (Eᶜ.indicator g) p μ
+      ≤ snorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ := by
+        unfold_let E; rw [compl_union, ← indicator_indicator]
+    _ ≤ snorm (Egᶜ.indicator g) p μ := snorm_indicator_le _
+    _ ≤ ε / 3 := hgε.le
+  have hmfnEc : AEStronglyMeasurable _ μ := ((hf n).indicator hmE.compl).aestronglyMeasurable
+  have hfnEcε : snorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3 := calc
+    snorm (Eᶜ.indicator (f n)) p μ
+      ≤ snorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ := by
+        unfold_let E; rw [compl_union, inter_comm, ← indicator_indicator]
+    _ ≤ snorm (Efᶜ.indicator (f n)) p μ := snorm_indicator_le _
+    _ ≤ ε / 3 := hfε n
+  have hmfngEc : AEStronglyMeasurable _ μ :=
+    (((hf n).sub hg).indicator hmE.compl).aestronglyMeasurable
+  have hfngEcε := calc
+    snorm (Eᶜ.indicator (f n - g)) p μ
+      = snorm (Eᶜ.indicator (f n) - Eᶜ.indicator g) p μ := by
+        rw [(Eᶜ.indicator_sub' _ _)]
+    _ ≤ snorm (Eᶜ.indicator (f n)) p μ + snorm (Eᶜ.indicator g) p μ := by
+        apply snorm_sub_le (by assumption) (by assumption) hp
+    _ ≤ ε / 3 + ε / 3 := add_le_add hfnEcε hgEcε
+  -- finally, combine interior and exterior estimates
+  calc
+    snorm (f n - g) p μ
+      = snorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ := by
+        congr; exact (E.indicator_compl_add_self _).symm
+    _ ≤ snorm (indicator Eᶜ (f n - g)) p μ + snorm (indicator E (f n - g)) p μ := by
+        apply snorm_add_le (by assumption) (by assumption) hp
+    _ ≤ (ε / 3 + ε / 3) + ε / 3 := add_le_add hfngEcε hfngEε
+    _ = ε := by simp only [ENNReal.add_thirds] --ENNReal.add_thirds ε
+
+/-- Lemma used in `tendsto_Lp_of_tendsto_ae`. -/
+private theorem ae_tendsto_ae_congr {f f' : ℕ → α → β} {g g' : α → β}
+    (hff' : ∀ (n : ℕ), f n =ᵐ[μ] f' n) (hgg' : g =ᵐ[μ] g')
+    (hfg : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
+    ∀ᵐ x ∂μ, Tendsto (fun n => f' n x) atTop (𝓝 (g' x)) := by
+  have hff'' := eventually_countable_forall.mpr hff'
+  filter_upwards [hff'', hgg', hfg] with x hff'x hgg'x hfgx
+  apply Tendsto.congr hff'x
+  rw [← hgg'x]; exact hfgx
+
+/-- Forward direction of Vitali's convergnece theorem, with a.e. instead of InMeasure convergence.-/
+theorem tendsto_Lp_of_tendsto_ae (hp : 1 ≤ p) (hp' : p ≠ ∞)
+    {f : ℕ → α → β} {g : α → β} (haef : ∀ n, AEStronglyMeasurable (f n) μ)
+    (hg' : Memℒp g p μ) (hui : UnifIntegrable f p μ) (hut : UnifTight f p μ)
+    (hfg : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
+    Tendsto (fun n => snorm (f n - g) p μ) atTop (𝓝 0) := by
+  -- come up with an a.e. equal strongly measurable replacement `f` for `g`
+  have hf := fun n => (haef n).stronglyMeasurable_mk
+  have hff' := fun n => (haef n).ae_eq_mk (μ := μ)
+  have hui' := hui.ae_eq hff'
+  have hut' := hut.aeeq hff'
+  have hg := hg'.aestronglyMeasurable.stronglyMeasurable_mk
+  have hgg' := hg'.aestronglyMeasurable.ae_eq_mk (μ := μ)
+  have hg'' := hg'.ae_eq hgg'
+  have haefg' := ae_tendsto_ae_congr hff' hgg' hfg
+  set f' := fun n => (haef n).mk (μ := μ)
+  set g' := hg'.aestronglyMeasurable.mk (μ := μ)
+  have haefg (n : ℕ) : f n - g =ᵐ[μ] f' n - g' := (hff' n).sub hgg'
+  have hsnfg (n : ℕ) := snorm_congr_ae (p := p) (haefg n)
+  apply Filter.Tendsto.congr (fun n => (hsnfg n).symm)
+  exact tendsto_Lp_of_tendsto_ae_of_meas hp hp' hf hg hg'' hui' hut' haefg'
+
+/-- Forward direction of Vitali's convergence theorem:
+if `f` is a sequence of uniformly integrable, uniformly tight functions that converge in
+measure to some function `g` in a finite measure space, then `f` converge in Lp to `g`. -/
+theorem tendsto_Lp_of_tendstoInMeasure (hp : 1 ≤ p) (hp' : p ≠ ∞)
+    (hf : ∀ n, AEStronglyMeasurable (f n) μ) (hg : Memℒp g p μ)
+    (hui : UnifIntegrable f p μ) (hut : UnifTight f p μ)
+    (hfg : TendstoInMeasure μ f atTop g) : Tendsto (fun n => snorm (f n - g) p μ) atTop (𝓝 0) := by
+  refine tendsto_of_subseq_tendsto fun ns hns => ?_
+  obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns
+  exact ⟨ms,
+    tendsto_Lp_of_tendsto_ae hp hp' (fun _ => hf _) hg
+      (fun ε hε => -- `UnifIntegrable` on a subsequence
+        let ⟨δ, hδ, hδ'⟩ := hui hε
+        ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
+      (fun ε hε => -- `UnifTight` on a subsequence
+        let ⟨s, hμs, hfε⟩ := hut hε
+        ⟨s, hμs, fun i => hfε _⟩)
+      hms'⟩
+
+/-- **Vitali's convergence theorem** (non-finite measure version).
+
+A sequence of functions `f` converges to `g` in Lp
+if and only if it is uniformly integrable, uniformly tight and converges to `g` in measure. -/
+theorem tendstoInMeasure_iff_tendsto_Lp (hp : 1 ≤ p) (hp' : p ≠ ∞)
+    (hf : ∀ n, Memℒp (f n) p μ) (hg : Memℒp g p μ) :
+    TendstoInMeasure μ f atTop g ∧ UnifIntegrable f p μ ∧ UnifTight f p μ
+      ↔ Tendsto (fun n => snorm (f n - g) p μ) atTop (𝓝 0) where
+  mp h := tendsto_Lp_of_tendstoInMeasure hp hp' (fun n => (hf n).1) hg h.2.1 h.2.2 h.1
+  mpr h := ⟨tendstoInMeasure_of_tendsto_snorm (lt_of_lt_of_le zero_lt_one hp).ne'
+        (fun n => (hf n).aestronglyMeasurable) hg.aestronglyMeasurable h,
+      unifIntegrable_of_tendsto_Lp hp hp' hf hg h,
+      unifTight_of_tendsto_Lp hp' hf hg h⟩
+
+end VitaliConvergence
 end MeasureTheory

Mathlib/MeasureTheory/Function/UniformIntegrable.lean

@@ -32,9 +32,9 @@ formulate the martingale convergence theorem.
 
 * `MeasureTheory.unifIntegrable_finite`: a finite sequence of Lp functions is uniformly
   integrable.
-* `MeasureTheory.tendsto_Lp_of_tendsto_ae`: a sequence of Lp functions which is uniformly
+* `MeasureTheory.tendsto_Lp_finite_of_tendsto_ae`: a sequence of Lp functions which is uniformly
   integrable converges in Lp if they converge almost everywhere.
-* `MeasureTheory.tendstoInMeasure_iff_tendsto_Lp`: Vitali convergence theorem:
+* `MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite`: Vitali convergence theorem:
   a sequence of Lp functions converges in Lp if and only if it is uniformly integrable
   and converges in measure.
 
@@ -132,6 +132,32 @@ protected theorem ae_eq (hf : UnifIntegrable f p μ) (hfg : ∀ n, f n =ᵐ[μ]
   filter_upwards [hfg n] with x hx
   simp_rw [Set.indicator_apply, hx]
 
+/-- Uniform integrability is preserved by restriction of the functions to a set. -/
+protected theorem indicator (hf : UnifIntegrable f p μ) (E : Set α) :
+    UnifIntegrable (fun i => E.indicator (f i)) p μ := fun ε hε ↦ by
+  obtain ⟨δ, hδ_pos, hε⟩ := hf hε
+  refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
+  calc
+    snorm (s.indicator (E.indicator (f i))) p μ = snorm (E.indicator (s.indicator (f i))) p μ := by
+      simp only [indicator_indicator, inter_comm]
+    _ ≤ snorm (s.indicator (f i)) p μ := snorm_indicator_le _
+    _ ≤ ENNReal.ofReal ε := hε _ _ hs hμs
+
+/-- Uniform integrability is preserved by restriction of the measure to a set. -/
+protected theorem restrict (hf : UnifIntegrable f p μ) (E : Set α) :
+    UnifIntegrable f p (μ.restrict E) := fun ε hε ↦ by
+  obtain ⟨δ, hδ_pos, hδε⟩ := hf hε
+  refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
+  rw [μ.restrict_apply hs, ← measure_toMeasurable] at hμs
+  calc
+    snorm (indicator s (f i)) p (μ.restrict E) = snorm (f i) p (μ.restrict (s ∩ E)) := by
+      rw [snorm_indicator_eq_snorm_restrict hs, μ.restrict_restrict hs]
+    _ ≤ snorm (f i) p (μ.restrict (toMeasurable μ (s ∩ E))) :=
+      snorm_mono_measure _ <| Measure.restrict_mono (subset_toMeasurable _ _) le_rfl
+    _ = snorm (indicator (toMeasurable μ (s ∩ E)) (f i)) p μ :=
+      (snorm_indicator_eq_snorm_restrict (measurableSet_toMeasurable _ _)).symm
+    _ ≤ ENNReal.ofReal ε := hδε i _ (measurableSet_toMeasurable _ _) hμs
+
 end UnifIntegrable
 
 theorem unifIntegrable_zero_meas [MeasurableSpace α] {p : ℝ≥0∞} {f : ι → α → β} :