Theorems · Theorem · probability

MeasureTheory.TendstoInDistribution.continuous_comp_prodMk_of_tendstoInMeasure_const

• 1000+ list: Slutsky's theorem

∀ {ι : 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}
  {Z : Ω' → E} {l : Filter ι} [inst_2 : SeminormedAddCommGroup E] [SecondCountableTopology E] [inst_4 : BorelSpace E]
  {E' : Type u_6} {F : Type u_7} {mE' : MeasurableSpace E'} [inst_5 : SeminormedAddCommGroup E']
  [SecondCountableTopology E'] [BorelSpace E'] [inst_8 : TopologicalSpace F] [inst_9 : MeasurableSpace F]
  [inst_10 : BorelSpace F] {g : E × E' → F},
  Continuous g →
    ∀ [l.IsCountablyGenerated] {X : ι → Ω'' → E} {Y : ι → Ω'' → E'} {c : E'},
      MeasureTheory.TendstoInDistribution X l Z (fun x => μ'') μ' →
        (MeasureTheory.TendstoInMeasure μ'' Y l fun x => c) →
          (∀ (i : ι), AEMeasurable (Y i) μ'') →
            MeasureTheory.TendstoInDistribution (fun n ω => g (X n ω, Y n ω)) l (fun ω => g (Z ω, c)) (fun x => μ'') μ'

Slutsky's theorem for a continuous function: if X n converges in distribution to Z, Y n converges in probability to a constant c, and g is a continuous function, then g (X n, Y n) converges in distribution to g (Z, c).

Defined in

Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasureSeminormedAddCommGroupSecondCountableTopologyBorelSpaceSeminormedAddCommGroupSecondCountableTopologyBorelSpaceTopologicalSpaceMeasurableSpaceBorelSpaceFilter.IsCountablyGenerated