levyProkhorovDist_pseudoMetricSpace_probabilityMeasure

Lean4

/-- The Lévy-Prokhorov distance `levyProkhorovDist` makes `ProbabilityMeasure Ω` a pseudometric
space. The instance is recorded on the type synonym
`LevyProkhorov (ProbabilityMeasure Ω) := ProbabilityMeasure Ω`.

Note: For this pseudometric to give the topology of convergence in distribution, one must
furthermore assume that `Ω` is separable. -/
noncomputable instance levyProkhorovDist_pseudoMetricSpace_probabilityMeasure :
    PseudoMetricSpace (LevyProkhorov (ProbabilityMeasure Ω))
    where
  dist μ ν := levyProkhorovDist μ.toMeasure ν.toMeasure
  dist_self _ := levyProkhorovDist_self _
  dist_comm _ _ := levyProkhorovDist_comm _ _
  dist_triangle _ _ _ := levyProkhorovDist_triangle _ _ _
  edist_dist μ ν := by simp [← ENNReal.ofReal_coe_nnreal]

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