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 variablesX : ℕ → Ω → ℝthat are independent, identically distributed with meanμand variancev, and a random variableY : Ω' → ℝfollowinggaussianReal 0 v, the sequencen ↦ (√n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * μ)converges toYin 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.