levyProkhorov_le_convergenceInDistribution

English

A neighborhood containment lemma for measures: for an open set G, small positive ε shifts the measure of G from P.toMeasure to nearby measures in nhds(P).

Русский

Лемма о поведении мер в окрестностях: для открытого множества G и малого ε мера P.toMeasure становится близкой к мерам Q.toMeasure в окрестности P.

LaTeX

$$$\\{Q : \\mathrm{ProbabilityMeasure}(Ω)\\,|\\, P.toMeasure G < Q.toMeasure G + ε\\} \\in \\mathcal{N}(P).$$$

Lean4

/-- The topology of the Lévy-Prokhorov metric is at least as fine as the topology of convergence in
distribution. -/
theorem levyProkhorov_le_convergenceInDistribution :
    TopologicalSpace.coinduced (LevyProkhorov.equiv (α := ProbabilityMeasure Ω)) inferInstance ≤
      (inferInstance : TopologicalSpace (ProbabilityMeasure Ω)) :=
  (LevyProkhorov.continuous_equiv_probabilityMeasure).coinduced_le

Похожие утверждения