English
A boundedness criterion for levyProkhorovDist μ ν ≤ δ: if for every measurable B and ε with δ<ε one has μ(B) ≤ ν(thickening ε B) + ε, then the Levy-Prokhorov distance is at most δ.
Русский
Условие, гарантирующее, что расстояние Леви–Прокхоров не превышает δ: для каждого измеримого множества B и ε с δ<ε выполняется μ(B) ≤ ν(thickening ε B) + ε.
LaTeX
$$$\\forall \\mu,\\nu : \\mathrm{Measure}(\\Omega)\\; [\\mathrm{IsProbabilityMeasure}\\,\\mu] [\\mathrm{IsProbabilityMeasure}\\,\\nu]\\; \\forall δ \\in \\mathbb{R},\\; (δ≥0) ∧ (∀ ε,B: δ<ε → ε<∞ → \\mathrm{Measurable}(B) → μ(B) ≤ ν(\\mathrm{thickening}(ε B)) + ε) \\, \\Rightarrow \\, \\operatorname{levyProkhorovDist}(\\mu,ν) ≤ δ.$$
Lean4
/-- A simple sufficient condition for bounding `levyProkhorovDist` between probability measures
from above. The condition involves only one of two natural bounds, the other bound is for free. -/
theorem levyProkhorovDist_le_of_forall_le (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {δ : ℝ}
(δ_nn : 0 ≤ δ) (h : ∀ ε B, δ < ε → MeasurableSet B → μ B ≤ ν (thickening ε B) + ENNReal.ofReal ε) :
levyProkhorovDist μ ν ≤ δ := by
apply toReal_le_of_le_ofReal δ_nn
apply levyProkhorovEDist_le_of_forall_le
intro ε B ε_gt ε_lt_top B_mble
have ε_gt' : δ < ε.toReal := by
refine (ofReal_lt_ofReal_iff ?_).mp ?_
· exact ENNReal.toReal_pos (ne_zero_of_lt ε_gt) ε_lt_top.ne
· simpa [ofReal_toReal_eq_iff.mpr ε_lt_top.ne] using ε_gt
convert h ε.toReal B ε_gt' B_mble
exact (ENNReal.ofReal_toReal ε_lt_top.ne).symm
