PMF

Mathlib.Probability.ProbabilityMassFunction.Basic

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

← MathLib Explorer

English

Support equals set of points with nonzero mass, equivalently.

Русский

Поддержка равно множеству точек с ненулевой массой.

LaTeX

$$$p.support = \{a : \alpha \mid p(a) \neq 0\}$$$

Lean4

/-- A probability mass function, or discrete probability measures is a function `α → ℝ≥0∞` such
  that the values have (infinite) sum `1`. -/
def PMF.{u} (α : Type u) : Type u :=
  { f : α → ℝ≥0∞ // HasSum f 1 }

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

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

Разделы

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

Аффилиация

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