levyProkhorov_eq_convergenceInDistribution

English

There is a homeomorphism between ProbabilityMeasure Ω and LevyProkhorov(ProbabilityMeasure Ω) given by LevyProkhorov.equiv.

Русский

Существует гомеоморфизм между ProbabilityMeasure Ω и LevyProkhorov(ProbabilityMeasure Ω), заданный LevyProkhorov.equiv.

LaTeX

$$$\\mathrm{homeomorphProbabilityMeasureLevyProkhorov}(Ω) : \\mathrm{ProbabilityMeasure}(Ω) \\simeq_t \\mathrm{LevyProkhorov}(\\mathrm{ProbabilityMeasure}(Ω)).$$$

Lean4

/-- The topology of the Lévy-Prokhorov metric on probability measures on a separable space
coincides with the topology of convergence in distribution. -/
theorem levyProkhorov_eq_convergenceInDistribution :
    (inferInstance : TopologicalSpace (ProbabilityMeasure Ω)) =
      TopologicalSpace.coinduced (LevyProkhorov.equiv _) inferInstance :=
  le_antisymm (LevyProkhorov.continuous_equiv_symm_probabilityMeasure (Ω := Ω)).coinduced_le
    levyProkhorov_le_convergenceInDistribution

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