levyProkhorovEDist_self — Mathlib

English

The Levy-Prokhorov distance between μ and ν is defined as levyProkhorovDist(μ,ν) = levyProkhorovEDist(μ,ν).toReal.

Русский

Расстояние Леви-Прокхоров между μ и ν задаётся как levyProkhorovDist(μ,ν) = levyProkhorovEDist(μ,ν).toReal.

LaTeX

$$$$ \operatorname{levyProkhorovDist}(\mu,\nu) = (\operatorname{levyProkhorovEDist}(\mu,\nu)).toReal. $$$$

Lean4

theorem levyProkhorovEDist_self (μ : Measure Ω) : levyProkhorovEDist μ μ = 0 :=
  by
  rw [← nonpos_iff_eq_zero, ← csInf_Ioo zero_lt_top]
  refine sInf_le_sInf fun ε ⟨hε₀, hε_top⟩ B _ ↦ and_self_iff.2 ?_
  refine le_add_right <| measure_mono <| self_subset_thickening ?_ _
  exact ENNReal.toReal_pos hε₀.ne' hε_top.ne

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