binomial_apply_zero

Mathlib.Probability.ProbabilityMassFunction.Binomial

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

English

For p ∈ ℝ≥0, p ≤ 1, and n ∈ ℕ, the binomial PMF at i = 0 equals (1-p)^n.

Русский

Для p ∈ ℝ≥0, p ≤ 1, n ∈ ℕ: binomial(p,h,n)(0) = (1-p)^n.

LaTeX

$$$\\text{binomial}(p,h,n)(0) = (1-p)^{n}$$$

Lean4

@[simp]
theorem binomial_apply_zero (p : ℝ≥0) (h : p ≤ 1) (n : ℕ) : binomial p h n 0 = (1 - p) ^ n := by simp [binomial_apply]

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

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

Разделы

Аффилиация

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