levyProkhorovEDist_le_of_forall_add_pos_le

English

Let μ, ν be measures on Ω. For any δ>0, if for all ε>δ and ε<∞ and measurable B, μ(B) ≤ ν(thickening ε.toReal B) + ε and ν(B) ≤ μ(thickening ε.toReal B) + ε, then levyProkhorovEDist μ ν ≤ δ.

Русский

Пусть μ, ν — меры на Ω. Для любого δ>0, если выполняются условия для всех ε>δ и ε<∞ и измеримых B, то levyProkhorovEDist μ ν ≤ δ.

LaTeX

$$$$ \ levyProkhorovEDist(\mu,\nu) \le δ. $$$$

Lean4

/-- A general sufficient condition for bounding `levyProkhorovEDist` from above. -/
theorem levyProkhorovEDist_le_of_forall_add_pos_le (μ ν : Measure Ω) (δ : ℝ≥0∞)
    (h :
      ∀ ε B,
        0 < ε →
          ε < ∞ →
            MeasurableSet B →
              μ B ≤ ν (thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (thickening (δ + ε).toReal B) + δ + ε) :
    levyProkhorovEDist μ ν ≤ δ := by
  apply ENNReal.le_of_forall_pos_le_add
  intro ε hε _
  by_cases ε_top : ε = ∞
  · simp only [ε_top, add_top, le_top]
  apply sInf_le
  intro B B_mble
  simpa only [add_assoc] using h ε B (coe_pos.mpr hε) coe_lt_top B_mble

Похожие утверждения