Theorems · Theorem · probability

ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum

∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω}
  {P' : MeasureTheory.Measure Ω'} {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} [inst : MeasureTheory.IsProbabilityMeasure P]
  [inst_1 : MeasureTheory.IsProbabilityMeasure P'],
  ProbabilityTheory.HasLaw Y (ProbabilityTheory.gaussianReal 0 1) P' →
    ∫ (x : Ω), X 0 x ∂P = 0 →
      ∫ (x : Ω), (X 0 ^ 2) x ∂P = 1 →
        ProbabilityTheory.iIndepFun X P →
          (∀ (i : ℕ), ProbabilityTheory.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.

Defined in

Mathlib.Probability.CentralLimitTheorem

Cited by

0 results in Mathlib

Foundations

Depth 295 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasure