noncomputable def stdGaussianDensity (x : ℝ) : ℝ

Density of the standard normal distribution N(0,1): φ(x) = (2π)^{-1/2} exp(-x²/2).

noncomputable def stdNormalMeasure : MeasureTheory.Measure ℝ

The standard normal probability measure on ℝ, defined as Lebesgue measure weighted by the standard Gaussian density stdGaussianDensity.

def ConvergesInDistributionRV {Ω : Type u_1} [MeasurableSpace Ω] (X : ℕ → Ω → ℝ) (P : MeasureTheory.Measure Ω) (ν : MeasureTheory.Measure ℝ) : Prop

A sequence of real random variables Xₙ : Ω → ℝ on a measure space (Ω, P) converges in distribution to a measure ν on ℝ if for every bounded continuous f : ℝ → ℝ, E[f(Xₙ)] → ∫ f dν (the Portmanteau characterization of weak convergence).

theorem central_limit_theorem {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X : ℕ → Ω → ℝ) (μ σ : ℝ) (hσ : 0 < σ) (hmeas : ∀ (i : ℕ), AEMeasurable (X i) P) (hmean : ∀ (i : ℕ), ∫ (x : Ω), X i x ∂P = μ) (hvar : ∀ (i : ℕ), ∫ (x : Ω), (X i x - μ) ^ 2 ∂P = σ ^ 2) (hindep : ProbabilityTheory.iIndepFun X P) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) P P) : ConvergesInDistributionRV (fun (n : ℕ) (ω : Ω) => (σ * √↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * μ)) P stdNormalMeasure

Central Limit Theorem. Let X₁, X₂, … be i.i.d. real random variables with mean μ and variance σ² ∈ (0, ∞). Set Sₙ = X₁ + … + Xₙ. Then the normalized sums (Sₙ − nμ)/(σ √n) converge in distribution to the standard normal distribution N(0, 1).