Theorems · Theorem · probability

ProbabilityTheory.strong_law_aux3

∀ {Ω : 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) →
      (fun n =>
          (∫ (a : Ω), (∑ i ∈ Finset.range n, ProbabilityTheory.truncation (X i) ↑i) a) -
            ↑n * ∫ (a : Ω), X 0 a) =o[Filter.atTop]
        Nat.cast

The expectation of the truncated version of Xᵢ behaves asymptotically like the whole expectation. This follows from convergence and Cesàro averaging.

Defined in

Mathlib.Probability.StrongLaw

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.MeasureSpaceMeasureTheory.IsProbabilityMeasure