Theorems · Theorem · probability

ProbabilityTheory.strong_law_aux2

∀ {Ω : 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 ω) →
          ∀ {c : ℝ},
            1 < c →
              ∀ᵐ (ω : Ω),
                (fun n =>
                    ∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) (↑i) ω -
                      ∫ (a : Ω),
                        (∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) ↑i) a) =o[Filter.atTop]
                  fun n => ↑⌊c ^ n⌋₊

The truncation of Xᵢ up to i satisfies the strong law of large numbers (with respect to the truncated expectation) along the sequence c^n, for any c > 1. This follows from strong_law_aux1 by varying ε.

Defined in

Mathlib.Probability.StrongLaw

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.MeasureSpaceMeasureTheory.IsProbabilityMeasure