Theorems · Theorem · probability

ProbabilityTheory.charFun_inv_sqrt_mul_sum

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ},
  ProbabilityTheory.iIndepFun X P →
    (∀ (i : ℕ), ProbabilityTheory.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

Defined in

Mathlib.Probability.CentralLimitTheorem

Cited by

1 results in Mathlib

Foundations

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