[Merged by Bors] - feat(probability/strong_law): Lp version of the strong law of large numbers

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
@@ -282,4 +283,41 @@ end
 
 end ident_distrib
 
+section uniform_integrable
+
+variables {E : Type*} [measurable_space E] [normed_group E] [borel_space E]
+  {μ : measure α} [is_finite_measure μ]
+
+lemma integrable.uniform_integrable_of_ident_distrib {ι : Type*} {f : ι → α → E}
+  {j : ι} (hj : integrable (f j) μ) (hfmeas : ∀ i, strongly_measurable (f i))
+  (hf : ∀ i, ident_distrib (f i) (f j) μ μ) :
+  uniform_integrable f 1 μ :=
+begin
+  refine uniform_integrable_of le_rfl ennreal.one_ne_top hfmeas (λ ε hε, _),
+  by_cases hι : nonempty ι,
+  swap, { exact ⟨0, λ i, false.elim (hι $ nonempty.intro i)⟩ },
+  obtain ⟨C, hC₁, hC₂⟩ :=
+    (mem_ℒp_one_iff_integrable.2 hj).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 hid : ident_distrib (λ x, ∥f i x∥₊) (λ x, ∥f j x∥₊) μ μ := (hf i).comp measurable_nnnorm,
+  have hpre : ∀ i, {x | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ∥f i x∥₊} =
+    (λ x, ∥f i x∥₊) ⁻¹' set.Ici (⟨C, hC₁.le⟩ : ℝ≥0),
+  { intro i,
+    ext x,
+    simp },
+  rw [snorm_one_eq_lintegral_nnnorm, snorm_one_eq_lintegral_nnnorm],
+  simp_rw [nnnorm_indicator_eq_indicator_nnnorm, ennreal.coe_indicator],
+  rw [lintegral_indicator _ (hmeas _), hpre i,
+    ← set_lintegral_map measurable_set_Ici measurable_coe_nnreal_ennreal
+      (hfmeas _).nnnorm.measurable, hid.map_eq,
+    set_lintegral_map measurable_set_Ici measurable_coe_nnreal_ennreal
+      (hfmeas _).nnnorm.measurable, ← hpre j],
+  simp_rw [← @nnreal.coe_le_coe ⟨C, hC₁.le⟩, subtype.coe_mk, coe_nnnorm],
+  rw [lintegral_indicator _ (measurable_set_le measurable_const (hfmeas _).norm.measurable)],
+end
+
+end uniform_integrable
+
 end probability_theory

src/probability/strong_law.lean

@@ -728,4 +728,90 @@ end
 
 end strong_law_ae
 
+section strong_law_L1
+
+variables {Ω : Type*} [measure_space Ω]
+
+/-- The averaging of a uniformly integrable sequence is also uniformly integrable. -/
+lemma uniform_integrable_average (μ : measure Ω)
+  (X : ℕ → Ω → ℝ) (hX : uniform_integrable X 1 μ) :
+  uniform_integrable (λ n, (∑ i in range n, X i) / n) 1 μ :=
+begin
+  obtain ⟨hX₁, hX₂, hX₃⟩ := hX,
+  refine ⟨λ n, _, λ ε hε, _, _⟩,
+  { simp_rw div_eq_mul_inv,
+    exact (strongly_measurable_sum' _ (λ i _, hX₁ i)).mul
+      (strongly_measurable_const : strongly_measurable (λ x, (↑n : ℝ)⁻¹)) },
+  { obtain ⟨δ, hδ₁, hδ₂⟩ := hX₂ hε,
+    refine ⟨δ, hδ₁, λ n s hs hle, _⟩,
+    simp_rw [div_eq_mul_inv, sum_mul, set.indicator_finset_sum],
+    refine le_trans (snorm_sum_le (λ i hi,
+      (((hX₁ i).mul_const (↑n)⁻¹).indicator hs).ae_strongly_measurable) le_rfl) _,
+    have : ∀ i, s.indicator (X i * (↑n)⁻¹) = (↑n : ℝ)⁻¹ • s.indicator (X i),
+    { intro i,
+      rw [mul_comm, (_ : (↑n)⁻¹ * X i = λ ω, (↑n : ℝ)⁻¹ • X i ω)],
+      { rw set.indicator_const_smul s (↑n)⁻¹ (X i),
+        refl },
+      { refl } },
+    simp_rw [this, snorm_const_smul, ← 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 ← card_range n },
+      exact 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⟩ := hX₃,
+    simp_rw [div_eq_mul_inv, sum_mul],
+    refine ⟨C, λ n, (snorm_sum_le (λ i hi,
+      ((hX₁ i).mul_const (↑n)⁻¹).ae_strongly_measurable) le_rfl).trans _⟩,
+    have : ∀ i, (λ ω, X i ω * (↑n)⁻¹) = (↑n : ℝ)⁻¹ • λ ω, X i ω,
+    { intro i,
+      ext ω,
+      simp only [mul_comm, pi.smul_apply, algebra.id.smul_eq_mul] },
+    simp_rw [this, snorm_const_smul, ← 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 ← card_range n },
+      exact 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
+
+variables [is_probability_measure (ℙ : measure Ω)]
+
+/-- *Strong law of large numbers*, L¹ version: if `X n` is a sequence of independent
+identically distributed integrable real-valued random variables, then `∑ i in range n, X i / n`
+converges in L¹ to `𝔼[X 0]`. -/
+theorem strong_law_L1
+  (X : ℕ → Ω → ℝ) (hmeas : ∀ i, strongly_measurable (X i)) (hint : integrable (X 0))
+  (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]) 1 ℙ) at_top (𝓝 0) :=
+begin
+  have havg : ∀ n, ae_strongly_measurable (λ ω, (∑ i in range n, X i ω) / n) ℙ,
+  { intro n,
+    refine strongly_measurable.ae_strongly_measurable _,
+    simp_rw div_eq_mul_inv,
+    exact strongly_measurable.mul_const (strongly_measurable_sum _  (λ i _, hmeas i)) _ },
+  refine tendsto_Lp_of_tendsto_in_measure _ le_rfl ennreal.one_ne_top 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 ℙ X $
+      integrable.uniform_integrable_of_ident_distrib hint hmeas hident).2.1 },
+  { ext n ω,
+    simp only [pi.coe_nat, pi.div_apply, sum_apply] }
+end
+
+end strong_law_L1
+
 end probability_theory