binomial_apply — Mathlib

English

For p ∈ ℝ≥0 with p ≤ 1, n ∈ ℕ, and i ∈ Fin(n+1), the binomial PMF satisfies binomial(p,h,n,i) = p^i (1-p)^{(n-i)} (n choose i).

Русский

Для p ∈ ℝ≥0, p ≤ 1, n ∈ ℕ, i ∈ Fin(n+1) выполняется binomial(p,h,n,i) = p^i (1-p)^{n-i} (n choose i).

LaTeX

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

Lean4

theorem binomial_apply (p : ℝ≥0) (h : p ≤ 1) (n : ℕ) (i : Fin (n + 1)) :
    binomial p h n i = p ^ (i : ℕ) * (1 - p) ^ ((Fin.last n - i) : ℕ) * (n.choose i : ℕ) := by simp [binomial]

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