Theorems · Theorem · probability

MeasureTheory.tendstoInDistribution_of_ae_tendsto

∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'}
  [inst : MeasureTheory.IsProbabilityMeasure μ'] {mE : MeasurableSpace E} {Z : Ω' → E} {l : Filter ι}
  [inst_1 : TopologicalSpace E] [l.IsCountablyGenerated] [inst_3 : OpensMeasurableSpace E] {X : ι → Ω' → E},
  (∀ (i : ι), AEMeasurable (X i) μ') →
    AEMeasurable Z μ' →
      (∀ᵐ (ω : Ω') ∂μ', Filter.Tendsto (fun i => X i ω) l (nhds (Z ω))) →
        MeasureTheory.TendstoInDistribution X l Z (fun x => μ') μ'

Almost sure convergence implies convergence in distribution.

Defined in

Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasureTopologicalSpaceFilter.IsCountablyGeneratedOpensMeasurableSpace