tsum_coe_indicator_ne_top

Mathlib.Probability.ProbabilityMassFunction.Basic

URI: https://scilib.ai/kg/mathlib#PMF.tsum_coe_indicator_ne_top

← MathLib Explorer

English

Membership in PMF support is equivalent to nonzero value.

Русский

Членство в поддержке PMF эквивалентно p(a) ≠ 0.

LaTeX

$$$a ∈ p.support ⇔ p(a) ≠ 0$$$

Lean4

theorem tsum_coe_indicator_ne_top (p : PMF α) (s : Set α) : ∑' a, s.indicator p a ≠ ∞ :=
  ne_of_lt
    (lt_of_le_of_lt (ENNReal.tsum_le_tsum (fun _ => Set.indicator_apply_le fun _ => le_rfl))
      (lt_of_le_of_ne le_top p.tsum_coe_ne_top))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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