Theorems · Theorem · probability

ProbabilityTheory.strong_law_aux5

∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) MeasureTheory.volume →
    (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) →
      (∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) →
        ∀ᵐ (ω : Ω),
          (fun n =>
              ∑ i ∈ Finset.range n, ProbabilityTheory.truncation (X i) (↑i) ω -
                ∑ i ∈ Finset.range n, X i ω) =o[Filter.atTop]
            fun n => ↑n

The truncated and non-truncated versions of Xᵢ have the same asymptotic behavior, as they almost surely coincide at all but finitely many steps. This follows from a probability computation and Borel-Cantelli.

Defined in

Mathlib.Probability.StrongLaw

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.MeasureSpaceMeasureTheory.IsProbabilityMeasure