English
The binomial PMF is the probability mass function for the number of successes in n independent Bernoulli trials with success probability p, defined on Fin(n+1) by i ↦ p^i (1-p)^{n-i} (n choose i).
Русский
Биномиальное распределение — это функция массы вероятностей числа успехов в n независимых испытаниях Бернулли с вероятностью успеха p, определённая на Fin(n+1) как i ↦ p^i (1-p)^{n-i} {n \\choose i}.
LaTeX
$$$\\text{binomial}(p,h,n) \\text{ is the PMF on } \\mathrm{Fin}(n+1)\\text{ with } (\\text{binomial}(p,h,n))(i) = p^{i} (1-p)^{(n-i)} {n \\choose i}$$$
Lean4
/-- The binomial `PMF`: the probability of observing exactly `i` “heads” in a sequence of `n`
independent coin tosses, each having probability `p` of coming up “heads”. -/
def binomial (p : ℝ≥0) (h : p ≤ 1) (n : ℕ) : PMF (Fin (n + 1)) :=
.ofFintype (fun i => ↑(p ^ (i : ℕ) * (1 - p) ^ ((Fin.last n - i) : ℕ) * (n.choose i : ℕ)))
(by
dsimp only
norm_cast
convert (add_pow p (1 - p) n).symm
· rw [Finset.sum_fin_eq_sum_range]
apply Finset.sum_congr rfl
intro i hi
rw [Finset.mem_range] at hi
rw [dif_pos hi]
· rw [add_tsub_cancel_of_le (mod_cast h), one_pow])
