dist_def — Mathlib

English

The Levy-Prokhorov distance between two measures on Ω coincides with the underlying distance between the corresponding measures after applying the probability-to-measure transformation.

Русский

Расстояние Леви–Прокхоров между двумя мерами на Ω совпадает с расстоянием между соответствующими мерами после применения перехода от вероятностной меры к мере.

LaTeX

$$$\\operatorname{dist}(\\mu,\\nu) = \\operatorname{levyProkhorovDist}(\\mu,\\nu) \\,\\text{ for }\\mu,\\nu \\text{ on } \\Omega.$$$

Lean4

theorem dist_def (μ ν : LevyProkhorov (ProbabilityMeasure Ω)) : dist μ ν = levyProkhorovDist μ.toMeasure ν.toMeasure :=
  rfl

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