levyProkhorovDist — Mathlib

English

The levyProkhorovDist is a real-valued distance between measures, defined via levyProkhorovEDist as its real realization.

Русский

Расстояние Леви-Прокхоров между мерами — вещественное, задаётся через реализацию levyProkhorovEDist.

LaTeX

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

Lean4

/-- The Lévy-Prokhorov distance between finite measures:
`d(μ,ν) = inf {r ≥ 0 | ∀ B, μ B ≤ ν Bᵣ + r ∧ ν B ≤ μ Bᵣ + r}`. -/
noncomputable def levyProkhorovDist (μ ν : Measure Ω) : ℝ :=
  (levyProkhorovEDist μ ν).toReal

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