feat: central limit theorem (leanprover-community#36208)

Prove the central limit theorem in dimension 1.

Co-authored-by: @hanwenzhu
Co-authored-by: Remy Degenne <remydegenne@gmail.com>
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Author: EtienneC30

Mathlib.lean

@@ -5996,6 +5996,7 @@ public import Mathlib.Order.Zorn
 public import Mathlib.Order.ZornAtoms
 public import Mathlib.Probability.BorelCantelli
 public import Mathlib.Probability.CDF
+public import Mathlib.Probability.CentralLimitTheorem
 public import Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
 public import Mathlib.Probability.CondVar
 public import Mathlib.Probability.ConditionalExpectation

Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

@@ -364,7 +364,6 @@ lemma tendsto_one_add_div_pow_exp (t : ℂ) :
     Tendsto (fun n : ℕ ↦ (1 + t / n) ^ n) atTop (𝓝 (exp t)) :=
   tendsto_one_add_div_cpow_exp t |>.comp tendsto_natCast_atTop_atTop |>.congr (by simp)
 
-set_option backward.isDefEq.respectTransparency false
 /-- `(1 + t/n + o(1/n)) ^ n → exp t` for `t ∈ ℂ`. -/
 lemma tendsto_pow_exp_of_isLittleO_sub_add_div {f : ℕ → ℂ} (t : ℂ)
     (hf : (fun n ↦ f n - (1 + t / n)) =o[atTop] fun n ↦ 1 / (n : ℂ)) :

Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean

@@ -6,6 +6,7 @@ Authors: Rémy Degenne
 module
 
 public import Mathlib.MeasureTheory.Measure.Portmanteau
+public import Mathlib.Probability.IdentDistrib
 
 /-!
 # Convergence in distribution
@@ -42,7 +43,7 @@ and convergence in distribution.
 
 @[expose] public section
 
-open Filter
+open Filter ProbabilityTheory
 open scoped Topology
 
 namespace MeasureTheory
@@ -74,6 +75,26 @@ lemma tendstoInDistribution_const [OpensMeasurableSpace E] (hZ : AEMeasurable Z
   forall_aemeasurable := fun _ ↦ by fun_prop
   tendsto := tendsto_const_nhds
 
+lemma tendstoInDistribution_of_identDistrib [OpensMeasurableSpace E] (i : ι)
+    (hX : ∀ j, IdentDistrib (X i) (X j) (μ i) (μ j)) (hZ : IdentDistrib (X i) Z (μ i) μ') :
+    TendstoInDistribution X l Z μ μ' where
+  forall_aemeasurable j := (hX j).aemeasurable_snd
+  aemeasurable_limit := hZ.aemeasurable_snd
+  tendsto := by
+    convert tendsto_const_nhds with j
+    exact (hX j).map_eq.symm.trans hZ.map_eq
+
+protected lemma TendstoInDistribution.congr [OpensMeasurableSpace E] {T : Ω' → E}
+    (hXY : ∀ i, X i =ᵐ[μ i] Y i) (hZT : Z =ᵐ[μ'] T) (h : TendstoInDistribution X l Z μ μ') :
+    TendstoInDistribution Y l T μ μ' where
+  forall_aemeasurable i := (h.forall_aemeasurable i).congr (hXY i)
+  aemeasurable_limit := h.aemeasurable_limit.congr hZT
+  tendsto := by
+    convert h.tendsto using 2 with n
+    · simpa using Measure.map_congr (hXY n).symm
+    · rw! [Measure.map_congr hZT]
+      rfl
+
 @[simp]
 lemma tendstoInDistribution_of_isEmpty [IsEmpty E] :
     TendstoInDistribution X l Z μ μ' where

Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean

@@ -31,7 +31,7 @@ public section
 
 
 open ProbabilityTheory Complex Set VectorFourier
-open scoped Nat RealInnerProductSpace
+open scoped Nat RealInnerProductSpace Topology
 
 namespace MeasureTheory
 
@@ -150,6 +150,17 @@ lemma taylorWithinEval_charFun_two_zero' (hX : AEMeasurable X P)
   any_goals fun_prop
   simp [← Pi.pow_apply, h1]
 
+lemma taylor_charFun_two (hX : AEMeasurable X P) (h0 : P[X] = 0) (h1 : P[X ^ 2] = 1) :
+    (fun t ↦ charFun (P.map X) t - (1 - t ^ 2 / 2)) =o[𝓝 0] fun t ↦ t ^ 2 := by
+  simp_rw [← taylorWithinEval_charFun_two_zero' (by fun_prop) h0 h1]
+  convert taylor_isLittleO_univ ?_
+  · simp
+  refine contDiff_charFun <|
+    (memLp_two_iff_integrable_sq (by fun_prop)).2 (.of_integral_ne_zero ?_)
+  rw [integral_map]
+  any_goals fun_prop
+  simp_all
+
 end Real
 
 end MeasureTheory

Mathlib/Probability/CentralLimitTheorem.lean

@@ -0,0 +1,154 @@
+/-
+Copyright (c) 2024 Thomas Zhu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Zhu, Etienne Marion
+-/
+module
+
+public import Mathlib.Probability.Distributions.Gaussian.Real
+public import Mathlib.MeasureTheory.Function.ConvergenceInDistribution
+
+import Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
+import Mathlib.MeasureTheory.Measure.LevyConvergence
+import Mathlib.Probability.Independence.CharacteristicFunction
+
+/-!
+# Central limit theorem
+
+We prove the central limit theorem in dimension 1.
+
+## Main statement
+
+* `tendstoInDistribution_inv_sqrt_mul_sum_sub`: Given a sequence of random variables
+  `X : ℕ → Ω → ℝ` that are independent, identically distributed with mean `μ` and variance `v`,
+  and a random variable `Y : Ω' → ℝ` following `gaussianReal 0 v`, the sequence
+  `n ↦ (√n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * μ)` converges to `Y` in distribution.
+
+## Tags
+
+central limit theorem
+-/
+
+public section
+
+noncomputable section
+
+open MeasureTheory ProbabilityTheory Complex Filter
+open scoped Real Topology
+
+namespace ProbabilityTheory
+
+variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
+  {P : Measure Ω} {P' : Measure Ω'} {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ}
+
+lemma charFun_inv_sqrt_mul_sum (hindep : iIndepFun X P)
+    (hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P) {n : ℕ} {t : ℝ} :
+    charFun (P.map (fun ω ↦ (√n)⁻¹ * ∑ k ∈ Finset.range n, X k ω)) t =
+      (charFun (P.map (X 0)) ((√n)⁻¹ * t)) ^ n := by
+  have mX n := (hident n).aemeasurable_fst
+  rw [charFun_map_mul_comp, (hindep.restrict _).charFun_map_fun_finset_sum_eq_prod (fun _  _↦ mX _)]
+  · simp [fun i ↦ (hident i).map_eq]
+  · exact Finset.aemeasurable_fun_sum _ fun _ _ ↦ mX _
+
+variable [IsProbabilityMeasure P]
+
+lemma tendsto_charFun_inv_sqrt_mul_pow {X : Ω → ℝ}
+    (hX : AEMeasurable X P) (h0 : P[X] = 0) (h1 : P[X ^ 2] = 1) (t : ℝ) :
+    Tendsto (fun (n : ℕ) ↦ (charFun (P.map X) ((√n)⁻¹ * t)) ^ n) atTop (𝓝 (exp (- t ^ 2 / 2))) := by
+  apply tendsto_pow_exp_of_isLittleO_sub_add_div
+  suffices (fun (n : ℕ) ↦ charFun (Measure.map X P) ((√n)⁻¹ * t) -
+      (1 + (-(((√n)⁻¹ * t) ^ 2 / 2) : ℂ))) =o[atTop] fun n ↦ ((√n)⁻¹ * t) ^ 2 by
+    have aux : (fun (n : ℕ) ↦ ‖(1 / n : ℂ)‖) = fun (n : ℕ) ↦ ‖(1 / n : ℝ)‖ := by simp
+    rw [← Asymptotics.isLittleO_norm_right, aux, Asymptotics.isLittleO_norm_right]
+    refine .of_const_mul_right (c := t ^ 2) ?_
+    convert this using 4 with n <;> norm_cast <;> simp [field]
+  have : Tendsto (fun (n : ℕ) ↦ (√n)⁻¹ * t) atTop (𝓝 0) := by
+    rw [← zero_mul t]
+    exact .mul_const t (tendsto_inv_atTop_zero.comp <| Real.tendsto_sqrt_atTop.comp <|
+      tendsto_natCast_atTop_atTop)
+  convert (taylor_charFun_two hX h0 h1).comp_tendsto this using 2
+  simp
+  ring
+
+variable [IsProbabilityMeasure P']
+
+/-- **Central Limit Theorem:** Given a sequence of random variables `X : ℕ → Ω → ℝ` that are
+independent, identically distributed, centered and with variance `1` and a random variable
+`Y : Ω' → ℝ` following `gaussianReal 0 1`, the sequence
+`n ↦ (√n)⁻¹ * ∑ k ∈ Finset.range n, X k` converges to `Y` in distribution. -/
+theorem tendstoInDistribution_inv_sqrt_mul_sum (hY : HasLaw Y (gaussianReal 0 1) P')
+    (h0 : P[X 0] = 0) (h1 : P[X 0 ^ 2] = 1) (hindep : iIndepFun X P)
+    (hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P) :
+    TendstoInDistribution (fun (n : ℕ) ω ↦ (√n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) atTop Y
+      (fun _ ↦ P) P' where
+  forall_aemeasurable n :=
+    .const_mul (Finset.aemeasurable_fun_sum _ fun _ _ ↦ (hident _).aemeasurable_fst) _
+  tendsto := by
+    refine ProbabilityMeasure.tendsto_iff_tendsto_charFun.2 fun t ↦ ?_
+    rw! [hY.map_eq]
+    simpa [charFun_inv_sqrt_mul_sum hindep hident, charFun_gaussianReal, neg_div] using
+      tendsto_charFun_inv_sqrt_mul_pow (hident 0).aemeasurable_fst h0 h1 t
+
+/-- **Central Limit Theorem:** Given a sequence of random variables `X : ℕ → Ω → ℝ` that are
+independent, identically distributed with mean `μ` and non-zero variance `v`, and a random variable
+`Y : Ω' → ℝ` following `gaussianReal 0 1`, the sequence
+`n ↦ (√(n * v)⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * μ)` converges to `Y` in distribution. -/
+private theorem tendstoInDistribution_inv_sqrt_mul_var_mul_sum_sub
+    (hY : HasLaw Y (gaussianReal 0 1) P')
+    (hX : Var[X 0; P] ≠ 0) (hindep : iIndepFun X P)
+    (hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P) :
+    TendstoInDistribution
+      (fun (n : ℕ) ω ↦ (√(n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * P[X 0]))
+      atTop Y (fun _ ↦ P) P' := by
+  have mX0 := (hident 0).aemeasurable_fst
+  have intX0 : Integrable (X 0) P := memLp_one_iff_integrable.1 <|
+    (memLp_two_of_variance_ne_zero mX0.aestronglyMeasurable hX).mono_exponent (by simp)
+  have this (n : ℕ) ω : (√(n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * P[X 0]) =
+      (√n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - P[X 0]) / √Var[X 0; P] := by
+    rw [← Finset.sum_div, Finset.sum_sub_distrib]
+    simp [field]
+  simp_rw [this]
+  convert tendstoInDistribution_inv_sqrt_mul_sum hY ?_ ?_ ?_ ?_
+  · rw [integral_div, integral_sub intX0 (by simp)]
+    simp
+  · simp only [Pi.pow_apply, div_pow]
+    rw [integral_div, ← variance_eq_integral mX0, Real.sq_sqrt (variance_nonneg _ _), div_self hX]
+  · exact hindep.comp (fun _ x ↦ (x - P[X 0]) / √Var[X 0; P]) (by fun_prop)
+  · convert fun n ↦ (hident n).comp (u := fun x ↦ (x - P[X 0]) / √Var[X 0; P]) (by fun_prop)
+
+/-- **Central Limit Theorem:** Given a sequence of random variables `X : ℕ → Ω → ℝ` that are
+independent, identically distributed with mean `μ` and variance `v`, and a random variable
+`Y : Ω' → ℝ` following `gaussianReal 0 v`, the sequence
+`n ↦ (√n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * μ)` converges to `Y` in distribution. -/
+theorem tendstoInDistribution_inv_sqrt_mul_sum_sub
+    (hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P')
+    (hX : MemLp (X 0) 2 P) (hindep : iIndepFun X P)
+    (hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P) :
+    TendstoInDistribution
+      (fun (n : ℕ) ω ↦ (√n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * P[X 0]))
+      atTop Y (fun _ ↦ P) P' := by
+  obtain h | h := eq_or_ne Var[X 0; P] 0
+  · have : ∀ᵐ ω ∂P, ∀ n, X n ω = P[X 0] := by
+      refine ae_all_iff.2 fun n ↦ ?_
+      convert (ae_eq_integral_of_variance_eq_zero ((hident n).memLp_iff.2 hX)) ?_ using 3
+      · rw [(hident n).integral_eq]
+      · rwa [(hident n).variance_eq]
+    have mX (n : ℕ) := (hident n).aemeasurable_fst
+    refine tendstoInDistribution_of_identDistrib 0 (fun n ↦ ?_) ?_
+    · refine ⟨by fun_prop, by fun_prop, Measure.map_congr ?_⟩
+      filter_upwards [this] with ω hω
+      simp [hω]
+    · exact ⟨by fun_prop, by fun_prop, by simp [hY.map_eq, h]⟩
+  have : HasLaw (fun ω ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P' := by
+    convert gaussianReal_div_const hY _
+    · simp
+    · ext; simp [h]
+  convert (tendstoInDistribution_inv_sqrt_mul_var_mul_sum_sub this h hindep hident).continuous_comp
+    (g := (√Var[X 0; P] * ·)) (by fun_prop)
+  · simp [field] -- simp [field, hX] triggers the unused simp arguments linter
+    field_simp [h]
+  · ext
+    simp [field] -- simp [field, hX] triggers the unused simp arguments linter
+    field_simp [h]
+
+end ProbabilityTheory

Mathlib/Probability/Moments/Variance.lean

@@ -132,6 +132,11 @@ lemma variance_of_not_memLp [IsFiniteMeasure μ] (hX : AEStronglyMeasurable X μ
     (hX_not : ¬ MemLp X 2 μ) :
     variance X μ = 0 := by simp [variance, (evariance_eq_top_iff hX).mpr hX_not]
 
+lemma memLp_two_of_variance_ne_zero [IsFiniteMeasure μ] (hX : AEStronglyMeasurable X μ)
+    (h : Var[X; μ] ≠ 0) : MemLp X 2 μ := by
+  contrapose! h
+  exact variance_of_not_memLp hX h
+
 theorem ofReal_variance [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :
     .ofReal (variance X μ) = evariance X μ := by
   rw [variance, ENNReal.ofReal_toReal]
@@ -150,6 +155,19 @@ lemma variance_eq_integral (hX : AEMeasurable X μ) : Var[X; μ] = ∫ ω, (X ω
   simp [variance, evariance, toReal_enorm, ← integral_toReal ((hX.sub_const _).enorm.pow_const _) <|
     .of_forall fun _ ↦ ENNReal.pow_lt_top enorm_lt_top]
 
+/-- A random variable with variance `0` is almost surely constant. -/
+lemma ae_eq_integral_of_variance_eq_zero [IsFiniteMeasure μ] (hX : MemLp X 2 μ)
+    (h : Var[X; μ] = 0) :
+    ∀ᵐ ω ∂μ, X ω = μ[X] := by
+  rw [variance_eq_integral hX.aemeasurable, integral_eq_zero_iff_of_nonneg] at h
+  · filter_upwards [h] with ω hω
+    simp at hω
+    grind
+  · exact fun _ ↦ by positivity
+  · simp_rw [sub_sq]
+    exact (hX.integrable_sq.sub (((hX.integrable (by simp)).const_mul _).mul_const _)).add
+      (integrable_const _)
+
 lemma variance_of_integral_eq_zero (hX : AEMeasurable X μ) (hXint : μ[X] = 0) :
     variance X μ = ∫ ω, X ω ^ 2 ∂μ := by
   simp [variance_eq_integral hX, hXint]
@@ -179,6 +197,7 @@ lemma covariance_self {X : Ω → ℝ} (hX : AEMeasurable X μ) :
   congr with x
   ring
 
+@[simp]
 theorem variance_nonneg (X : Ω → ℝ) (μ : Measure Ω) : 0 ≤ variance X μ :=
   ENNReal.toReal_nonneg
 

docs/100.yaml

@@ -193,6 +193,8 @@
   authors: Thomas Zhu
 47:
   title  : The Central Limit Theorem
+  decl   : ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub
+  authors: Thomas Zhu, Rémy Degenne, Etienne Marion
 48:
   title  : Dirichlet’s Theorem
   decl   : Nat.infinite_setOf_prime_and_eq_mod

docs/1000.yaml

@@ -135,7 +135,9 @@ Q190391X:
 
 Q190391:
   title: Central limit theorem
-  # in 100.yaml also
+  decl: ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub
+  authors: Thomas Zhu, Rémy Degenne, Etienne Marion
+  date: 2026
 
 Q190556:
   title: De Moivre's theorem