English
For finite measures μ, ν, κ on Ω, levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ.
Русский
Для мер μ, ν, κ на Ω выполняется неравенство треугольника: d(μ,κ) ≤ d(μ,ν) + d(ν,κ).
LaTeX
$$$$ \operatorname{levyProkhorovDist}(\mu,\kappa) \le \operatorname{levyProkhorovDist}(\mu,\nu) + \operatorname{levyProkhorovDist}(\nu,\kappa). $$$$
Lean4
theorem levyProkhorovEDist_triangle [OpensMeasurableSpace Ω] (μ ν κ : Measure Ω) :
levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ :=
by
by_cases LPμν_finite : levyProkhorovEDist μ ν = ∞
· simp [LPμν_finite]
by_cases LPνκ_finite : levyProkhorovEDist ν κ = ∞
· simp [LPνκ_finite]
apply levyProkhorovEDist_le_of_forall_add_pos_le
intro ε B ε_pos ε_lt_top B_mble
have half_ε_pos : 0 < ε / 2 := ENNReal.div_pos ε_pos.ne' ofNat_ne_top
let r := levyProkhorovEDist μ ν + ε / 2
let s := levyProkhorovEDist ν κ + ε / 2
have lt_r : levyProkhorovEDist μ ν < r := lt_add_right LPμν_finite half_ε_pos.ne'
have lt_s : levyProkhorovEDist ν κ < s := lt_add_right LPνκ_finite half_ε_pos.ne'
have hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε := by
simp_rw [s, r, add_assoc, add_comm (ε / 2), add_assoc, ENNReal.add_halves, ← add_assoc,
add_comm (levyProkhorovEDist μ ν)]
have hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal :=
by
rw [← hs_add_r, ← ENNReal.toReal_add]
· finiteness
· finiteness
rw [← hs_add_r', add_assoc, ← hs_add_r, add_assoc _ _ ε, ← hs_add_r]
refine ⟨?_, ?_⟩
·
calc
μ B ≤ ν (thickening r.toReal B) + r := left_measure_le_of_levyProkhorovEDist_lt lt_r B_mble
_ ≤ κ (thickening s.toReal (thickening r.toReal B)) + s + r :=
(add_le_add_right (left_measure_le_of_levyProkhorovEDist_lt lt_s isOpen_thickening.measurableSet) _)
_ = κ (thickening s.toReal (thickening r.toReal B)) + (s + r) := (add_assoc _ _ _)
_ ≤ κ (thickening (s.toReal + r.toReal) B) + (s + r) :=
add_le_add_right (measure_mono (thickening_thickening_subset _ _ _)) _
·
calc
κ B ≤ ν (thickening s.toReal B) + s := right_measure_le_of_levyProkhorovEDist_lt lt_s B_mble
_ ≤ μ (thickening r.toReal (thickening s.toReal B)) + r + s :=
(add_le_add_right (right_measure_le_of_levyProkhorovEDist_lt lt_r isOpen_thickening.measurableSet) s)
_ = μ (thickening r.toReal (thickening s.toReal B)) + (s + r) := by rw [add_assoc, add_comm r]
_ ≤ μ (thickening (r.toReal + s.toReal) B) + (s + r) :=
(add_le_add_right (measure_mono (thickening_thickening_subset _ _ _)) _)
_ = μ (thickening (s.toReal + r.toReal) B) + (s + r) := by rw [add_comm r.toReal]
