Theorems · Theorem · probability

ProbabilityTheory.strong_law_ae_simpleFunc_comp

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : MeasurableSpace E]
  (X : ℕ → Ω → E),
  Measurable (X 0) →
    Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) →
        ∀ (φ : MeasureTheory.SimpleFunc E E),
          ∀ᵐ (ω : Ω) ∂μ,
            Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) Filter.atTop
              (nhds (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))

Preliminary lemma for the strong law of large numbers for vector-valued random variables: the composition of the random variables with a simple function satisfies the strong law of large numbers.

Defined in

Mathlib.Probability.StrongLaw

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasureNormedAddCommGroupNormedSpaceCompleteSpaceMeasurableSpace