feat(probability/strong_law): Lp version of the strong law of large n…

…umbers (#15392)

This PR proves the Lp version of the strong law of large numbers which states that $\frac{1}{n}\sum_{i < n} X_i$ converges to $\mathbb{E}[X_0]$ in the Lp-norm where $(X_n)$ is iid. and Lp.

src/measure_theory/function/uniform_integrable.lean

@@ -42,7 +42,7 @@ uniform integrable, uniformly absolutely continuous integral, Vitali convergence
 -/
 
 noncomputable theory
-open_locale classical measure_theory nnreal ennreal topological_space
+open_locale classical measure_theory nnreal ennreal topological_space big_operators
 
 namespace measure_theory
 
@@ -943,6 +943,60 @@ lemma uniform_integrable_iff [is_finite_measure μ] (hp : 1 ≤ p) (hp' : p ≠
 ⟨λ h, ⟨h.1, λ ε, h.spec (lt_of_lt_of_le ennreal.zero_lt_one hp).ne.symm hp'⟩,
  λ h, uniform_integrable_of hp hp' h.1 h.2⟩
 
+
+/-- The averaging of a uniformly integrable sequence is also uniformly integrable. -/
+lemma uniform_integrable_average (hp : 1 ≤ p)
+  {f : ℕ → α → ℝ} (hf : uniform_integrable f p μ) :
+  uniform_integrable (λ n, (∑ i in finset.range n, f i) / n) p μ :=
+begin
+  obtain ⟨hf₁, hf₂, hf₃⟩ := hf,
+  refine ⟨λ n, _, λ ε hε, _, _⟩,
+  { simp_rw div_eq_mul_inv,
+    exact (finset.ae_strongly_measurable_sum' _ (λ i _, hf₁ i)).mul
+      (ae_strongly_measurable_const : ae_strongly_measurable (λ x, (↑n : ℝ)⁻¹) μ) },
+  { obtain ⟨δ, hδ₁, hδ₂⟩ := hf₂ hε,
+    refine ⟨δ, hδ₁, λ n s hs hle, _⟩,
+    simp_rw [div_eq_mul_inv, finset.sum_mul, set.indicator_finset_sum],
+    refine le_trans (snorm_sum_le (λ i hi, ((hf₁ i).mul_const (↑n)⁻¹).indicator hs) hp) _,
+    have : ∀ i, s.indicator (f i * (↑n)⁻¹) = (↑n : ℝ)⁻¹ • s.indicator (f i),
+    { intro i,
+      rw [mul_comm, (_ : (↑n)⁻¹ * f i = λ ω, (↑n : ℝ)⁻¹ • f i ω)],
+      { rw set.indicator_const_smul s (↑n)⁻¹ (f i),
+        refl },
+      { refl } },
+    simp_rw [this, snorm_const_smul, ← finset.mul_sum, nnnorm_inv, real.nnnorm_coe_nat],
+    by_cases hn : (↑(↑n : ℝ≥0)⁻¹ : ℝ≥0∞) = 0,
+    { simp only [hn, zero_mul, zero_le] },
+    refine le_trans _ (_ : ↑(↑n : ℝ≥0)⁻¹ * (n • ennreal.of_real ε) ≤ ennreal.of_real ε),
+    { refine (ennreal.mul_le_mul_left hn ennreal.coe_ne_top).2 _,
+      conv_rhs { rw ← finset.card_range n },
+      exact finset.sum_le_card_nsmul _ _ _ (λ i hi, hδ₂ _ _ hs hle) },
+    { simp only [ennreal.coe_eq_zero, inv_eq_zero, nat.cast_eq_zero] at hn,
+      rw [nsmul_eq_mul, ← mul_assoc, ennreal.coe_inv, ennreal.coe_nat,
+        ennreal.inv_mul_cancel _ ennreal.coe_nat_ne_top, one_mul],
+      { exact le_rfl },
+      all_goals { simpa only [ne.def, nat.cast_eq_zero] } } },
+  { obtain ⟨C, hC⟩ := hf₃,
+    simp_rw [div_eq_mul_inv, finset.sum_mul],
+    refine ⟨C, λ n, (snorm_sum_le (λ i hi, (hf₁ i).mul_const (↑n)⁻¹) hp).trans _⟩,
+    have : ∀ i, (λ ω, f i ω * (↑n)⁻¹) = (↑n : ℝ)⁻¹ • λ ω, f i ω,
+    { intro i,
+      ext ω,
+      simp only [mul_comm, pi.smul_apply, algebra.id.smul_eq_mul] },
+    simp_rw [this, snorm_const_smul, ← finset.mul_sum, nnnorm_inv, real.nnnorm_coe_nat],
+    by_cases hn : (↑(↑n : ℝ≥0)⁻¹ : ℝ≥0∞) = 0,
+    { simp only [hn, zero_mul, zero_le] },
+    refine le_trans _ (_ : ↑(↑n : ℝ≥0)⁻¹ * (n • C : ℝ≥0∞) ≤ C),
+    { refine (ennreal.mul_le_mul_left hn ennreal.coe_ne_top).2 _,
+      conv_rhs { rw ← finset.card_range n },
+      exact finset.sum_le_card_nsmul _ _ _ (λ i hi, hC i) },
+    { simp only [ennreal.coe_eq_zero, inv_eq_zero, nat.cast_eq_zero] at hn,
+      rw [nsmul_eq_mul, ← mul_assoc, ennreal.coe_inv, ennreal.coe_nat,
+        ennreal.inv_mul_cancel _ ennreal.coe_nat_ne_top, one_mul],
+      { exact le_rfl },
+      all_goals { simpa only [ne.def, nat.cast_eq_zero] } } }
+end
+
 end uniform_integrable
 
 end measure_theory

src/probability/ident_distrib.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import probability.variance
+import measure_theory.function.uniform_integrable
 
 /-!
 # Identically distributed random variables
@@ -107,6 +108,12 @@ protected lemma comp {u : γ → δ} (h : ident_distrib f g μ ν) (hu : measura
   ident_distrib (u ∘ f) (u ∘ g) μ ν :=
 h.comp_of_ae_measurable hu.ae_measurable
 
+protected lemma of_ae_eq {g : α → γ} (hf : ae_measurable f μ) (heq : f =ᵐ[μ] g) :
+  ident_distrib f g μ μ :=
+{ ae_measurable_fst := hf,
+  ae_measurable_snd := hf.congr heq,
+  map_eq := measure.map_congr heq }
+
 lemma measure_mem_eq (h : ident_distrib f g μ ν) {s : set γ} (hs : measurable_set s) :
   μ (f ⁻¹' s) = ν (g ⁻¹' s) :=
 by rw [← measure.map_apply_of_ae_measurable h.ae_measurable_fst hs,
@@ -283,4 +290,58 @@ end
 
 end ident_distrib
 
+section uniform_integrable
+
+open topological_space
+
+variables {E : Type*} [measurable_space E] [normed_add_comm_group E] [borel_space E]
+  [second_countable_topology E] {μ : measure α} [is_finite_measure μ]
+
+/-- This lemma is superceded by `mem_ℒp.uniform_integrable_of_ident_distrib` which only require
+`ae_strongly_measurable`. -/
+lemma mem_ℒp.uniform_integrable_of_ident_distrib_aux {ι : Type*} {f : ι → α → E}
+  {j : ι} {p : ℝ≥0∞} (hp : 1 ≤ p) (hp' : p ≠ ∞)
+  (hℒp : mem_ℒp (f j) p μ) (hfmeas : ∀ i, strongly_measurable (f i))
+  (hf : ∀ i, ident_distrib (f i) (f j) μ μ) :
+  uniform_integrable f p μ :=
+begin
+  refine uniform_integrable_of' hp hp' hfmeas (λ ε hε, _),
+  by_cases hι : nonempty ι,
+  swap, { exact ⟨0, λ i, false.elim (hι $ nonempty.intro i)⟩ },
+  obtain ⟨C, hC₁, hC₂⟩ := hℒp.snorm_indicator_norm_ge_pos_le μ (hfmeas _) hε,
+  have hmeas : ∀ i, measurable_set {x | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ∥f i x∥₊} :=
+    λ i, measurable_set_le measurable_const (hfmeas _).measurable.nnnorm,
+  refine ⟨⟨C, hC₁.le⟩, λ i, le_trans (le_of_eq _) hC₂⟩,
+  have : {x : α | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ∥f i x∥₊}.indicator (f i) =
+    (λ x : E, if (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ∥x∥₊ then x else 0) ∘ (f i),
+  { ext x,
+    simp only [set.indicator, set.mem_set_of_eq] },
+  simp_rw [coe_nnnorm, this],
+  rw [← snorm_map_measure _ (hf i).ae_measurable_fst, (hf i).map_eq,
+    snorm_map_measure _ (hf j).ae_measurable_fst],
+  { refl },
+  all_goals { exact ae_strongly_measurable_id.indicator
+      (measurable_set_le measurable_const measurable_nnnorm) },
+end
+
+/-- A sequence of identically distributed Lᵖ functions is p-uniformly integrable. -/
+lemma mem_ℒp.uniform_integrable_of_ident_distrib {ι : Type*} {f : ι → α → E}
+  {j : ι} {p : ℝ≥0∞} (hp : 1 ≤ p) (hp' : p ≠ ∞)
+  (hℒp : mem_ℒp (f j) p μ) (hf : ∀ i, ident_distrib (f i) (f j) μ μ) :
+  uniform_integrable f p μ :=
+begin
+  have hfmeas : ∀ i, ae_strongly_measurable (f i) μ :=
+    λ i, (hf i).ae_strongly_measurable_iff.2 hℒp.1,
+  set g : ι → α → E := λ i, (hfmeas i).some,
+  have hgmeas : ∀ i, strongly_measurable (g i) := λ i, (Exists.some_spec $ hfmeas i).1,
+  have hgeq : ∀ i, g i =ᵐ[μ] f i := λ i, (Exists.some_spec $ hfmeas i).2.symm,
+  have hgℒp : mem_ℒp (g j) p μ := hℒp.ae_eq (hgeq j).symm,
+  exact uniform_integrable.ae_eq (mem_ℒp.uniform_integrable_of_ident_distrib_aux hp hp'
+    hgℒp hgmeas $
+    λ i, (ident_distrib.of_ae_eq (hgmeas i).ae_measurable (hgeq i)).trans ((hf i).trans
+      $ ident_distrib.of_ae_eq (hfmeas j).ae_measurable (hgeq j).symm)) hgeq,
+end
+
+end uniform_integrable
+
 end probability_theory

src/probability/strong_law.lean

@@ -19,6 +19,10 @@ If `X n` is a sequence of independent identically distributed integrable real-va
 variables, then `∑ i in range n, X i / n` converges almost surely to `𝔼[X 0]`.
 We give here the strong version, due to Etemadi, that only requires pairwise independence.
 
+This file also contains the Lᵖ version of the strong law of large numbers provided by
+`probability_theory.strong_law_Lp` which shows `∑ i in range n, X i / n` converges in Lᵖ to
+`𝔼[X 0]` provided `X n` is independent identically distributed and is Lᵖ.
+
 ## Implementation
 
 We follow the proof by Etemadi
@@ -728,4 +732,36 @@ end
 
 end strong_law_ae
 
+section strong_law_Lp
+
+variables {Ω : Type*} [measure_space Ω] [is_probability_measure (ℙ : measure Ω)]
+
+/-- *Strong law of large numbers*, Lᵖ version: if `X n` is a sequence of independent
+identically distributed real-valued random variables in Lᵖ, then `∑ i in range n, X i / n`
+converges in Lᵖ to `𝔼[X 0]`. -/
+theorem strong_law_Lp
+  {p : ℝ≥0∞} (hp : 1 ≤ p) (hp' : p ≠ ∞)
+  (X : ℕ → Ω → ℝ) (hℒp : mem_ℒp (X 0) p)
+  (hindep : pairwise (λ i j, indep_fun (X i) (X j)))
+  (hident : ∀ i, ident_distrib (X i) (X 0)) :
+  tendsto (λ n, snorm (λ ω, (∑ i in range n, X i ω) / n - 𝔼[X 0]) p ℙ) at_top (𝓝 0) :=
+begin
+  have hmeas : ∀ i, ae_strongly_measurable (X i) ℙ :=
+    λ i, (hident i).ae_strongly_measurable_iff.2 hℒp.1,
+  have hint : integrable (X 0) ℙ := hℒp.integrable hp,
+  have havg : ∀ n, ae_strongly_measurable (λ ω, (∑ i in range n, X i ω) / n) ℙ,
+  { intro n,
+    simp_rw div_eq_mul_inv,
+    exact ae_strongly_measurable.mul_const (ae_strongly_measurable_sum _  (λ i _, hmeas i)) _ },
+  refine tendsto_Lp_of_tendsto_in_measure _ hp hp' havg (mem_ℒp_const _) _
+    (tendsto_in_measure_of_tendsto_ae havg (strong_law_ae _ hint hindep hident)),
+  rw (_ : (λ n ω, (∑ i in range n, X i ω) / ↑n) = λ n, (∑ i in range n, X i) / ↑n),
+  { exact (uniform_integrable_average hp $
+      mem_ℒp.uniform_integrable_of_ident_distrib hp hp' hℒp hident).2.1 },
+  { ext n ω,
+    simp only [pi.coe_nat, pi.div_apply, sum_apply] }
+end
+
+end strong_law_Lp
+
 end probability_theory