left_measure_le_of_levyProkhorovEDist_lt

English

If levyProkhorovEDist μ ν < c for μ, ν measures and B is measurable, then ν(B) ≤ μ(thickening(c.toReal B)) + c.

Русский

Пусть μ, ν — меры на Ω и B — измеримое множество. Если levyProkhorovEDist(μ,ν) < c, то ν(B) ≤ μ(thickening(c.toReal B)) + c.

LaTeX

$$$$ \nu(B) \le \mu\bigl(\mathrm{thickening}(c^{\toReal})(B)\bigr) + c, \quad B \text{ измеримо}. $$$$

Lean4

theorem left_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).1

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