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

Equations
Instances For
theorem PMF.binomial_apply (p : ENNReal) (h : p 1) (n : ) (i : Fin (n + 1)) :
(PMF.binomial p h n) i = p ^ i * (1 - p) ^ (() - i) * (n.choose 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_last (p : ENNReal) (h : p 1) (n : ) :
(PMF.binomial p h n) () = p ^ n
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 : Bool) => bif x then 1 else 0) ()

The binomial distribution on one coin is the bernoully distribution.