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

theorem ProbabilityTheory.charFun_inv_sqrt_mul_sum {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} (hindep : iIndepFun X P) (hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P) {n : ℕ} {t : ℝ} : MeasureTheory.charFun (MeasureTheory.Measure.map (fun (ω : Ω) => (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) t = MeasureTheory.charFun (MeasureTheory.Measure.map (X 0) P) ((√↑n)⁻¹ * t) ^ n

theorem ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → ℝ} (hX : AEMeasurable X P) (h0 : ∫ (x : Ω), X x ∂P = 0) (h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1) (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.charFun (MeasureTheory.Measure.map X P) ((√↑n)⁻¹ * t) ^ n) Filter.atTop (nhds (Complex.exp (-↑t ^ 2 / 2)))

theorem ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω} {P' : MeasureTheory.Measure Ω'} {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure P'] (hY : HasLaw Y (gaussianReal 0 1) P') (h0 : ∫ (x : Ω), X 0 x ∂P = 0) (h1 : ∫ (x : Ω), (X 0 ^ 2) x ∂P = 1) (hindep : iIndepFun X P) (hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P) : MeasureTheory.TendstoInDistribution (fun (n : ℕ) (ω : Ω) => (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) Filter.atTop Y (fun (x : ℕ) => P) 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 ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω} {P' : MeasureTheory.Measure Ω'} {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure P'] (hY : HasLaw Y (gaussianReal 0 (variance (X 0) P).toNNReal) P') (hX : MeasureTheory.MemLp (X 0) 2 P) (hindep : iIndepFun X P) (hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P) : MeasureTheory.TendstoInDistribution (fun (n : ℕ) (ω : Ω) => (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)) Filter.atTop Y (fun (x : ℕ) => P) P'

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.