Binomial random variables

This file defines the binomial distribution and binomial random variables, and computes their expectation and variance.

Main definitions

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

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)

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.

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.

instance ProbabilityTheory.isProbabilityMeasure_binomial {n : ℕ} {p : ↑unitInterval} : MeasureTheory.IsProbabilityMeasure (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

Binomial random variables