Theorems · Theorem · probability

ProbabilityTheory.strong_law_aux7

∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) MeasureTheory.volume →
    Pairwise (Function.onFun (fun f g => ProbabilityTheory.IndepFun f g MeasureTheory.volume) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) →
        (∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) →
          ∀ᵐ (ω : Ω),
            Filter.Tendsto (fun n => (∑ i ∈ Finset.range n, X i ω) / ↑n) Filter.atTop (nhds (∫ (a : Ω), X 0 a))

Xᵢ satisfies the strong law of large numbers along all integers. This follows from the corresponding fact along the sequences c^n, and the fact that any integer can be sandwiched between c^n and c^(n+1) with comparably small error if c is close enough to 1 (which is formalized in tendsto_div_of_monotone_of_tendsto_div_floor_pow).

Defined in

Mathlib.Probability.StrongLaw

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.MeasureSpaceMeasureTheory.IsProbabilityMeasure