right_measure_le_of_levyProkhorovEDist_lt

English

Let μ, ν be measures on Ω and δ ≥ 0. If for all ε>0, ε<∞ and measurable B, μ(B) ≤ ν(B^ε) + δ + ε and ν(B) ≤ μ(B^ε) + δ + ε, then levyProkhorovEDist μ ν ≤ δ.

Русский

Пусть μ, ν — меры на Ω и δ ≥ 0. Если для всех ε > 0, ε < ∞ и измеримых B верно μ(B) ≤ ν(B^ε) + δ + ε и ν(B) ≤ μ(B^ε) + δ + ε, то levyProkhorovEDist μ ν ≤ δ.

LaTeX

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

Lean4

theorem right_measure_le_of_levyProkhorovEDist_lt {μ ν : Measure Ω} {c : ℝ≥0∞} (h : levyProkhorovEDist μ ν < c)
    {B : Set Ω} (B_mble : MeasurableSet B) : ν B ≤ μ (thickening c.toReal B) + c :=
  by
  obtain ⟨c', ⟨hc', lt_c⟩⟩ := sInf_lt_iff.mp h
  exact meas_le_of_le_of_forall_le_meas_thickening_add ν μ lt_c.le (hc' B B_mble).2

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