Documentation

Mathlib.Probability.ProbabilityMassFunction.Binomial

The binomial distribution #

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

Main results #

source
@[deprecated ProbabilityTheory.binomial (since := "2026-04-07")]
def PMF.binomial (p : NNReal) (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
    source
    @[deprecated ProbabilityTheory.binomial_real_singleton (since := "2026-04-07")]
    theorem PMF.binomial_apply (p : NNReal) (h : p ≤ 1) (n : ℕ) (i : Fin (n + 1)) :
    (binomial p h n) i = ↑p ^ ↑i * (1 - ↑p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i)
    source
    @[deprecated ProbabilityTheory.binomial_real_zero (since := "2026-04-07")]
    theorem PMF.binomial_apply_zero (p : NNReal) (h : p ≤ 1) (n : ℕ) :
    (binomial p h n) 0 = (1 - ↑p) ^ n
    source
    @[deprecated ProbabilityTheory.binomial_real_self (since := "2026-04-07")]
    theorem PMF.binomial_apply_last (p : NNReal) (h : p ≤ 1) (n : ℕ) :
    (binomial p h n) (Fin.last n) = ↑p ^ n
    source
    @[deprecated ProbabilityTheory.binomial_real_self (since := "2026-04-07")]
    theorem PMF.binomial_apply_self (p : NNReal) (h : p ≤ 1) (n : ℕ) :
    (binomial p h n) (Fin.last n) = ↑p ^ n
    source
    @[deprecated ProbabilityTheory.binomial_one_eq_bernoulliMeasure (since := "2026-05-31")]
    theorem PMF.binomial_one_eq_bernoulli (p : NNReal) (h : p ≤ 1) :
    binomial p h 1 = map (fun (x : Bool) => bif x then 1 else 0) (bernoulli p h)

    The binomial distribution on one coin is the Bernoulli distribution.

    source
    @[deprecated ProbabilityTheory.binomial_singleton (since := "2026-04-07")]
    theorem PMF.binomial_apply_of_le {k b : ℕ} (hb : k ≤ b) {x : NNReal} (h : x ≤ 1) :
    ENNReal.ofReal (↑(b.choose k) * ↑x ^ k * (1 - ↑x) ^ (b - k)) = (binomial x h b) (Fin.ofNat (b + 1) k)