English
A simple sufficient condition for bounding levyProkhorovEDist from above: if μ and ν are probability measures and for a given δ there holds μ(B) ≤ ν(thickening ε B) + ε for all ε,B, then levyProkhorovEDist μ ν ≤ δ.
Русский
Упрощённое условие сверху для расстояния Леви–Прокхоров: если две вероятностные меры удовлетворяют неравенству μ(B) ≤ ν(thickening ε B) + ε для всех B и ε, то расстояние ≤ δ.
LaTeX
$$$\\forall \\mu,\\nu : \\mathrm{Measure}(\\Omega)\\;[\\mathrm{IsProbabilityMeasure}\\,\\mu]\\,[\\mathrm{IsProbabilityMeasure}\\,\\nu]\\; (\\delta \\in \\mathbb{R}_{+}) \\, (h) : \\, \\operatorname{levyProkhorovEDist}(\\mu,\\nu) ≤ δ \\,\\text{ provided } \\forall ε,B: δ<ε → ε<∞ → \\text{Measurable}(B) → μ(B) ≤ ν(\\mathrm{thickening}(ε B)) + ε.$$$
Lean4
/-- A simple sufficient condition for bounding `levyProkhorovEDist` between probability measures
from above. The condition involves only one of two natural bounds, the other bound is for free. -/
theorem levyProkhorovEDist_le_of_forall_le (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
(δ : ℝ≥0∞) (h : ∀ ε B, δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε) :
levyProkhorovEDist μ ν ≤ δ := by
apply levyProkhorovEDist_le_of_forall μ ν δ
intro ε B ε_gt ε_lt_top B_mble
refine ⟨h ε B ε_gt ε_lt_top B_mble, ?_⟩
have B_subset := subset_compl_thickening_compl_thickening_self ε.toReal B
apply (measure_mono (μ := ν) B_subset).trans
rw [prob_compl_eq_one_sub isOpen_thickening.measurableSet]
have Tc_mble := (isOpen_thickening (δ := ε.toReal) (E := B)).isClosed_compl.measurableSet
specialize h ε (thickening ε.toReal B)ᶜ ε_gt ε_lt_top Tc_mble
rw [prob_compl_eq_one_sub isOpen_thickening.measurableSet] at h
have almost := add_le_add (c := μ (thickening ε.toReal B)) h rfl.le
rw [tsub_add_cancel_of_le prob_le_one, add_assoc] at almost
apply (tsub_le_tsub_right almost _).trans
rw [ENNReal.add_sub_cancel_left (measure_ne_top ν _), add_comm ε]
