Theorems · Theorem · probability

ProbabilityTheory.strong_law_aux4

∀ {Ω : 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) ω -
                      ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 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 original expectation) along the sequence c^n, for any c > 1. This follows from the version from the truncated expectation, and the fact that the truncated and the original expectations have the same asymptotic behavior.

Defined in

Mathlib.Probability.StrongLaw

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.MeasureSpaceMeasureTheory.IsProbabilityMeasure