English
Let μ, ν be measures on Ω and δ > 0. If for all ε>0 and B measurable, μ(B) ≤ ν(thickening(δ+ε).toReal B) + ε and ν(B) ≤ μ(thickening(δ+ε).toReal B) + ε, then levyProkhorovEDist μ ν ≤ δ.
Русский
Пусть μ, ν — меры на Ω и δ > 0. Если для любого ε>0 и измеримого B выполняются μ(B) ≤ ν(thickening(δ+ε).toReal B) + ε и ν(B) ≤ μ(thickening(δ+ε).toReal B) + ε, то levyProkhorovEDist μ ν ≤ δ.
LaTeX
$$$$ \ levyProkhorovEDist(\mu,\nu) \le δ. $$$$
Lean4
/-- A simple general sufficient condition for bounding `levyProkhorovEDist` from above. -/
theorem levyProkhorovEDist_le_of_forall (μ ν : Measure Ω) (δ : ℝ≥0∞)
(h :
∀ ε B,
δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε) :
levyProkhorovEDist μ ν ≤ δ := by
by_cases δ_top : δ = ∞
· simp only [δ_top, le_top]
apply levyProkhorovEDist_le_of_forall_add_pos_le
intro x B x_pos x_lt_top B_mble
simpa only [← add_assoc] using
h (δ + x) B (ENNReal.lt_add_right δ_top x_pos.ne.symm)
(by simp only [add_lt_top, Ne.lt_top δ_top, x_lt_top, and_self]) B_mble
