meas_le_of_le_of_forall_le_meas_thickening_add

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

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

Lean4

theorem meas_le_of_le_of_forall_le_meas_thickening_add {ε₁ ε₂ : ℝ≥0∞} (μ ν : Measure Ω) (h_le : ε₁ ≤ ε₂) {B : Set Ω}
    (hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁) : μ B ≤ ν (thickening ε₂.toReal B) + ε₂ :=
  by
  by_cases ε_top : ε₂ = ∞
  · simp only [ε_top, toReal_top, add_top, le_top]
  apply hε₁.trans (add_le_add ?_ h_le)
  exact measure_mono (μ := ν) (thickening_mono (toReal_mono ε_top h_le) B)

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