The binomial distribution #
This file defines the probability mass function of the binomial distribution.
Main results #
binomial_one_eq_bernoulli
: Forn = 1
, it is equal toPMF.bernoulli
.
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”.
Equations
- PMF.binomial p h n = PMF.ofFintype (fun (i : Fin (n + 1)) => p ^ ↑i * (1 - p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i)) ⋯