prob_compl_lt_one_sub_of_lt_prob — Mathlib

English

Let p be an extended nonnegative real with p < μ(s) for a measurable set s. Then μ(s^c) < 1 - p, provided μ is zero-or-probability.

Русский

Пусть p < μ(s) для измеримого множества s. Тогда μ(s^c) < 1 - p, если μ — нулевая или вероятностная мера.

LaTeX

$$$p < \mu(s) \implies \mu(s^c) < 1 - p$$$

Lean4

theorem prob_compl_lt_one_sub_of_lt_prob {p : ℝ≥0∞} (hμs : p < μ s) (s_mble : MeasurableSet s) : μ sᶜ < 1 - p :=
  by
  rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
  · simp at hμs
  · rw [prob_compl_eq_one_sub s_mble]
    apply ENNReal.sub_lt_of_sub_lt prob_le_one (Or.inl one_ne_top)
    convert hμs
    exact ENNReal.sub_sub_cancel one_ne_top (lt_of_lt_of_le hμs prob_le_one).le

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