English
There exists a continuous equivalence between LevyProkhorov.equiv and its inverse, relating probability measures to their Levy-Prokhorov representations.
Русский
Существует непрерывное эквивалентное отображение между эквивалентностью Леви–Прокхоровой и её обратной, связывающее вероятностные меры с их представлениями.
LaTeX
$$$\\mathrm{continuous}\\_equiv\\_symm\\_probabilityMeasure$$$
Lean4
/-- The identity map is a homeomorphism from `ProbabilityMeasure Ω` with the topology of
convergence in distribution to `ProbabilityMeasure Ω` with the Lévy-Prokhorov (pseudo)metric. -/
noncomputable def homeomorph_probabilityMeasure_levyProkhorov :
ProbabilityMeasure Ω ≃ₜ LevyProkhorov (ProbabilityMeasure Ω)
where
toFun := LevyProkhorov.equiv _
invFun := (LevyProkhorov.equiv _).symm
left_inv := congrFun rfl
right_inv := congrFun rfl
continuous_toFun := LevyProkhorov.continuous_equiv_symm_probabilityMeasure
continuous_invFun := LevyProkhorov.continuous_equiv_probabilityMeasure
