binomial_apply_last

Mathlib.Probability.ProbabilityMassFunction.Binomial

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

English

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

Русский

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

LaTeX

$$$\\text{binomial}(p,h,n)(\\mathrm{last}(n)) = p^{n}$$$

Lean4

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

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

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

Разделы

Аффилиация

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