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
.
@[simp]
theorem
Pmf.binomial_apply_zero
(p : ENNReal)
(h : p ≤ 1)
(n : ℕ)
:
↑(Pmf.binomial p h n) 0 = (1 - p) ^ n
@[simp]
theorem
Pmf.binomial_one_eq_bernoulli
(p : ENNReal)
(h : p ≤ 1)
:
Pmf.binomial p h 1 = Pmf.map (fun x => bif x then 1 else 0) (Pmf.bernoulli p h)
The binomial distribution on one coin is the bernoully distribution.