ae_iff_prob_eq_one

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ae_iff_prob_eq_one

English

For hp measurable predicate, (∀ᵐ a, p(a)) iff μ{a | p(a)} = 1.

Русский

Для измеримого предиката p, (для почти всех a) p(a) эквивалентно μ{a | p(a)} = 1.

LaTeX

$$$\text{Measurable}(p) \Rightarrow (\forall\!a, p(a)\text{ а.е.}) \iff \mu\{a \mid p(a)\} = 1$$$

Lean4

theorem ae_iff_prob_eq_one (hp : Measurable p) : (∀ᵐ a ∂μ, p a) ↔ μ {a | p a} = 1 :=
  mem_ae_iff_prob_eq_one hp.setOf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru