Theorems · Theorem · probability

MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_sub

∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {m' : MeasurableSpace Ω'}
  {μ' : MeasureTheory.Measure Ω'} [inst : MeasureTheory.IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''}
  {μ'' : MeasureTheory.Measure Ω''} [inst_1 : MeasureTheory.IsProbabilityMeasure μ''] {mE : MeasurableSpace E}
  {l : Filter ι} [inst_2 : SeminormedAddCommGroup E] [SecondCountableTopology E] [inst_4 : BorelSpace E]
  {X : ι → Ω'' → E} [l.IsCountablyGenerated] (Y : ι → Ω'' → E) (Z : Ω' → E),
  MeasureTheory.TendstoInDistribution X l Z (fun x => μ'') μ' →
    MeasureTheory.TendstoInMeasure μ'' (Y - X) l 0 →
      (∀ (i : ι), AEMeasurable (Y i) μ'') → MeasureTheory.TendstoInDistribution Y l Z (fun x => μ'') μ'

Let X, Y be two sequences of measurable functions such that X n converges in distribution to Z, and Y n - X n converges in probability to 0. Then Y n converges in distribution to Z.

Defined in

Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasureSeminormedAddCommGroupSecondCountableTopologyBorelSpaceFilter.IsCountablyGenerated