The binomial distribution

This file defines the probability mass function of the binomial distribution.

Main results

• binomial_one_eq_bernoulli: For n = 1, it is equal to Pmf.bernoulli.

noncomputable def Pmf.binomial (p : ENNReal) (h : p ≤ 1) (n : ℕ) : Pmf (Fin (n + 1))

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”.

theorem Pmf.binomial_apply (p : ENNReal) (h : p ≤ 1) (n : ℕ) (i : Fin (n + 1)) : ↑(Pmf.binomial p h n) i = p ^ ↑i * (1 - p) ^ (↑(Fin.last n) - ↑i) * ↑(Nat.choose n ↑i)

@[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_apply_self (p : ENNReal) (h : p ≤ 1) (n : ℕ) : ↑(Pmf.binomial p h n) ↑n = p ^ n

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.