English
For open measurable Ω and finite measures μ, ν, κ on Ω, levyProkhorovDist satisfies triangle inequality.
Русский
Для открытого пространства Ω и конечных мер μ, ν, κ расстояние Леви-Прокхоров удовлетворяет неравенству треугольника.
LaTeX
$$$$ \operatorname{levyProkhorovDist}(\mu,\kappa) \le \operatorname{levyProkhorovDist}(\mu,\nu) + \operatorname{levyProkhorovDist}(\nu,\kappa). $$$$
Lean4
theorem levyProkhorovDist_triangle [OpensMeasurableSpace Ω] (μ ν κ : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
[IsFiniteMeasure κ] : levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ :=
by
have dμν_finite := (levyProkhorovEDist_lt_top μ ν).ne
have dνκ_finite := (levyProkhorovEDist_lt_top ν κ).ne
convert ENNReal.toReal_mono ?_ <| levyProkhorovEDist_triangle μ ν κ
· simp only [levyProkhorovDist, ENNReal.toReal_add dμν_finite dνκ_finite]
· exact ENNReal.add_ne_top.mpr ⟨dμν_finite, dνκ_finite⟩
