Theorems · Theorem · probability

ProbabilityTheory.strong_law_ae_real

∀ {Ω : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) μ →
    Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) →
        ∀ᵐ (ω : Ω) ∂μ,
          Filter.Tendsto (fun n => (∑ i ∈ Finset.range n, X i ω) / ↑n) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))

Strong law of large numbers, almost sure version: if X n is a sequence of independent identically distributed integrable real-valued random variables, then ∑ i ∈ range n, X i / n converges almost surely to 𝔼[X 0]. We give here the strong version, due to Etemadi, that only requires pairwise independence. Superseded by strong_law_ae, which works for random variables taking values in any Banach space.

Defined in

Mathlib.Probability.StrongLaw

Cited by

2 results in Mathlib

Foundations

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