Documentation

Mathlib.Probability.Distributions.Binomial

Binomial random variables #

This file defines the binomial distribution and binomial random variables, and computes their expectation and variance. For n : ℕ and p : I, the binomial distribution Bin(n, p) is defined as the cardinal of a random subset U of Set.Iic n such that each k ∈ Set.Iic n belongs to U independently with probability p.

Main definition #

ProbabilityTheory.binomial: Binomial distribution on an arbitrary semiring with parameters n and p.

Implementation details #

We provide the definition binomial with notation Bin(n, P) as the corresponding measure over ℕ. We also introduce a notation Bin(R, n p) for the same measure but over a general AddMonoidWithOne R, that stands for Bin(n, p).map (Nat.cast : ℕ → R). This is in particular useful if one is interested in the binomial distribution as a measure over ℝ or ℤ. Results should be proven for both Bin(n, p) and Bin(R, n, p) when possible, using the first one to prove the second. Note that results concerning Bin(R, n, p) may require [MeasurableSingletonClass R] and/or [CharZero R].

When refering to Bin(n, p) in names, use binomial. When refering to Bin(R, n, p), use map_cast_binomial.

Notation #

Bin(n, p) is the binomial distribution with parameters n and p in ℕ. Bin(R, n, p) is the binomial distribution with parameters n and p in R.

noncomputable def ProbabilityTheory.binomial (n : ℕ) (p : ↑unitInterval) :

MeasureTheory.Measure ℕ

The binomial probability distribution with parameter p.

Equations

ProbabilityTheory.binomial n p = MeasureTheory.Measure.map Set.ncard (ProbabilityTheory.setBernoulli (Set.Iio n) p)

Instances For

def ProbabilityTheory.«termBin(_,_)» :

Lean.ParserDescr

The binomial probability distribution with parameter p.

Equations

One or more equations did not get rendered due to their size.

Instances For

def ProbabilityTheory.«termBin(_,_,_)» :

Lean.ParserDescr

The binomial probability distribution with parameter p valued in the semiring R.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ProbabilityTheory.binomial_nat {n : ℕ} {p : ↑unitInterval} :

MeasureTheory.Measure.map Nat.cast (binomial n p) = binomial n p

theorem ProbabilityTheory.binomial_zero {p : ↑unitInterval} :

binomial 0 p = MeasureTheory.Measure.dirac 0

@[simp]

theorem ProbabilityTheory.map_cast_binomial_zero {R : Type u_1} [MeasurableSpace R] [AddMonoidWithOne R] {p : ↑unitInterval} :

MeasureTheory.Measure.map Nat.cast (binomial 0 p) = MeasureTheory.Measure.dirac 0

instance ProbabilityTheory.isProbabilityMeasure_binomial {n : ℕ} {p : ↑unitInterval} :

MeasureTheory.IsProbabilityMeasure (binomial n p)

instance ProbabilityTheory.isProbabilityMeasure_map_cast_binomial {R : Type u_1} [MeasurableSpace R] [AddMonoidWithOne R] {n : ℕ} {p : ↑unitInterval} :

MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map Nat.cast (binomial n p))

theorem ProbabilityTheory.ae_le_of_hasLaw_binomial {Ω : Type u_2} {m : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {n : ℕ} {p : ↑unitInterval} {X : Ω → ℕ} (hX : HasLaw X (binomial n p) P) :

∀ᵐ (ω : Ω) ∂P, X ω ≤ n

theorem ProbabilityTheory.binomial_real_singleton (n k : ℕ) (p : ↑unitInterval) :

(binomial n p).real {k} = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

theorem ProbabilityTheory.binomial_singleton (n k : ℕ) (p : ↑unitInterval) :

(binomial n p) {k} = ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k))

theorem ProbabilityTheory.map_cast_binomial_real_singleton {R : Type u_1} [MeasurableSpace R] [AddMonoidWithOne R] [MeasurableSingletonClass R] [CharZero R] (n k : ℕ) (p : ↑unitInterval) :

(MeasureTheory.Measure.map Nat.cast (binomial n p)).real {↑k} = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

@[simp]

theorem ProbabilityTheory.binomial_nonneg {n : ℕ} {p : ↑unitInterval} {k : ℕ} :

0 ≤ ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

theorem ProbabilityTheory.map_cast_binomial_singleton {R : Type u_1} [MeasurableSpace R] [AddMonoidWithOne R] [MeasurableSingletonClass R] [CharZero R] (n k : ℕ) (p : ↑unitInterval) :

(MeasureTheory.Measure.map Nat.cast (binomial n p)) {↑k} = ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k))

@[simp]

theorem ProbabilityTheory.binomial_real_zero (n : ℕ) (p : ↑unitInterval) :

(binomial n p).real {0} = (1 - ↑p) ^ n

@[simp]

theorem ProbabilityTheory.map_cast_binomial_real_zero {R : Type u_1} [MeasurableSpace R] [AddMonoidWithOne R] [MeasurableSingletonClass R] [CharZero R] (n : ℕ) (p : ↑unitInterval) :

(MeasureTheory.Measure.map Nat.cast (binomial n p)).real {0} = (1 - ↑p) ^ n

@[simp]

theorem ProbabilityTheory.binomial_real_self (n : ℕ) (p : ↑unitInterval) :

(binomial n p).real {n} = ↑p ^ n

@[simp]

theorem ProbabilityTheory.map_cast_binomial_real_self {R : Type u_1} [MeasurableSpace R] [AddMonoidWithOne R] [MeasurableSingletonClass R] [CharZero R] (n : ℕ) (p : ↑unitInterval) :

(MeasureTheory.Measure.map Nat.cast (binomial n p)).real {↑n} = ↑p ^ n

@[simp]

theorem ProbabilityTheory.binomial_one_eq_bernoulliMeasure (p : ↑unitInterval) :

binomial 1 p = bernoulliMeasure 1 0 p

theorem ProbabilityTheory.binomial_eq_sum_dirac (n : ℕ) (p : ↑unitInterval) :

binomial n p = ∑ k ∈ Finset.Iic n, ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • MeasureTheory.Measure.dirac k

theorem ProbabilityTheory.map_cast_binomial_eq_sum_dirac {R : Type u_1} [MeasurableSpace R] [AddMonoidWithOne R] [MeasurableSingletonClass R] (n : ℕ) (p : ↑unitInterval) :

MeasureTheory.Measure.map Nat.cast (binomial n p) = ∑ k ∈ Finset.Iic n, ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • MeasureTheory.Measure.dirac ↑k

theorem ProbabilityTheory.integrable_map_cast_binomial {R : Type u_1} [MeasurableSpace R] [AddMonoidWithOne R] {n : ℕ} {p : ↑unitInterval} {E : Type u_3} [NormedAddCommGroup E] [MeasurableSingletonClass R] (f : R → E) :

MeasureTheory.Integrable f (MeasureTheory.Measure.map Nat.cast (binomial n p))

theorem ProbabilityTheory.integrable_binomial {n : ℕ} {p : ↑unitInterval} {E : Type u_3} [NormedAddCommGroup E] (f : ℕ → E) :

MeasureTheory.Integrable f (binomial n p)

theorem ProbabilityTheory.integral_binomial {n : ℕ} {p : ↑unitInterval} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : ℕ → E) :

∫ (x : ℕ), f x ∂binomial n p = ∑ k ∈ Finset.Iic n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f k

theorem ProbabilityTheory.integral_map_cast_binomial {R : Type u_1} [MeasurableSpace R] [AddMonoidWithOne R] {n : ℕ} {p : ↑unitInterval} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSingletonClass R] (f : R → E) :

∫ (x : R), f x ∂MeasureTheory.Measure.map Nat.cast (binomial n p) = ∑ k ∈ Finset.Iic n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f ↑k

Binomial random variables #