levyProkhorovDist_pseudoMetricSpace_finiteMeasure

Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

URI: https://scilib.ai/kg/mathlib#MeasureTheory.levyProkhorovDist_pseudoMetricSpace_finiteMeasure

Lean4

/-- The Lévy-Prokhorov distance `levyProkhorovDist` makes `FiniteMeasure Ω` a pseudometric
space. The instance is recorded on the type synonym
`LevyProkhorov (FiniteMeasure Ω) := FiniteMeasure Ω`. -/
noncomputable instance levyProkhorovDist_pseudoMetricSpace_finiteMeasure :
    PseudoMetricSpace (LevyProkhorov (FiniteMeasure Ω))
    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]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru