Theorems · Theorem · probability

MeasureTheory.tendstoInDistribution_const

∀ {ι : 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] [inst_2 : OpensMeasurableSpace E],
  AEMeasurable Z μ' → MeasureTheory.TendstoInDistribution (fun x => Z) l Z (fun x => μ') μ'

Defined in

Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasureTopologicalSpaceOpensMeasurableSpace