Multinomial distribution

DefinitionMultinomial mass function#✓fully proved

The multinomial mass function: the probability N! / ∏ᵢ xᵢ! · ∏ᵢ pᵢ ^ xᵢ that N independent throws, landing in cell i with probability pᵢ, produce the cell counts x; it is 0 unless ∑ᵢ xᵢ = N. The formula is a polynomial in p and is defined for every real vector p; it is a probability mass function when p is a probability vector (0 ≤ pᵢ, ∑ᵢ pᵢ = 1), which the normalization theorems assume. The converse does not hold in general: for N = 0 it is the point mass at the zero vector for every p, even vectors that are not probability vectors.

noncomputable def multinomialReal (N : ℕ) (p : ι → ℝ) (x : ι → ℕ) : ℝ :=
  if ∑ i, x i = N then (Nat.multinomial univ x : ℝ) * ∏ i, p i ^ x i else 0

Used by 16

Used byPoisson conditioning · Multinomial distribution as a probability mass function · Mass of the multinomial distribution at a count vector · Multinomial mass formula on the simplex · Nonnegativity of the multinomial mass function · Support of the multinomial mass lies in the antidiagonal · Multinomial mass vanishes off the simplex · Covariance · Mixed second moment · Second factorial moment, polynomial form · Mean · Mean, polynomial form · Second factorial moment · Second factorial moment, polynomial form · Normalization · Multinomial theorem

TheoremNonnegativity of the multinomial mass function#✓fully proved

The multinomial mass function is nonnegative for a nonnegative vector p.

theorem multinomialReal_nonneg {N : ℕ} {p : ι → ℝ} (hp : ∀ i, 0 ≤ p i) (x : ι → ℕ) :
    0 ≤ multinomialReal N p x

Uses 1 · Used by 1

Statement usesMultinomial mass function

Used byMultinomial distribution as a probability mass function

TheoremMultinomial mass vanishes off the simplex#✓fully proved

The multinomial mass function vanishes off the simplex ∑ᵢ xᵢ = N.

theorem multinomialReal_of_sum_ne {N : ℕ} {p : ι → ℝ} {x : ι → ℕ} (h : ∑ i, x i ≠ N) :
    multinomialReal N p x = 0

Uses 1 · Used by 2

Statement usesMultinomial mass function

Used byPoisson conditioning · Support of the multinomial mass lies in the antidiagonal

TheoremMultinomial mass formula on the simplex#✓fully proved

On the simplex the multinomial mass is N! / ∏ᵢ xᵢ! · ∏ᵢ pᵢ ^ xᵢ.

theorem multinomialReal_eq_factorial_div {N : ℕ} {p : ι → ℝ} {x : ι → ℕ}
    (h : ∑ i, x i = N) :
    multinomialReal N p x = (N.factorial : ℝ) / (∏ i, ((x i).factorial : ℝ)) * ∏ i, p i ^ x i

Uses 1 · Used by 1

Statement usesMultinomial mass function

Used byPoisson conditioning

18 fully proved

Support

TheoremSupport of the multinomial mass lies in the antidiagonal#✓fully proved

The multinomial mass function vanishes outside the finite set piAntidiag univ N of count vectors with total N: the support is contained in the antidiagonal. Equality of the support with the antidiagonal needs all p i > 0 (e.g. for p = (1, 0), N = 1 the vector (0, 1) is in the antidiagonal but has mass 0).

theorem multinomialReal_of_notMem {N : ℕ} {p : ι → ℝ} {x : ι → ℕ}
    (h : x ∉ piAntidiag univ N) : multinomialReal N p x = 0

Uses 2 · Used by 1

Statement usesMultinomial mass function

Proof usesMultinomial mass vanishes off the simplex

Used byMultinomial distribution as a probability mass function

TheoremMultinomial theorem#✓fully proved

∑ₓ P(x) = (∑ᵢ pᵢ) ^ N for every real vector p.

theorem sum_multinomialReal_eq_pow (N : ℕ) (p : ι → ℝ) :
    ∑ x ∈ piAntidiag univ N, multinomialReal N p x = (∑ i, p i) ^ N

Uses 1 · Used by 3

Statement usesMultinomial mass function

Used byPoisson conditioning · Mean, polynomial form · Normalization

TheoremNormalization#✓fully proved

For ∑ᵢ pᵢ = 1 the multinomial masses sum to one.

theorem sum_multinomialReal {N : ℕ} {p : ι → ℝ} (hp : ∑ i, p i = 1) :
    ∑ x ∈ piAntidiag univ N, multinomialReal N p x = 1

Uses 2 · Used by 2

Statement usesMultinomial mass function

Proof usesMultinomial theorem

Used byMultinomial distribution as a probability mass function · Covariance

DefinitionMultinomial distribution as a probability mass function#✓fully proved

The multinomial law of N throws with cell probabilities p (a probability vector), as a probability mass function on count vectors ι → ℕ.

noncomputable def multinomial (N : ℕ) (p : ι → ℝ) (hp₀ : ∀ i, 0 ≤ p i) (hp₁ : ∑ i, p i = 1) :
    PMF (ι → ℕ) :=
  PMF.ofFinset (fun x => ENNReal.ofReal (multinomialReal N p x)) (piAntidiag univ N)
    (by
      rw [← ENNReal.ofReal_sum_of_nonneg fun x _ => multinomialReal_nonneg hp₀ x,
        sum_multinomialReal hp₁, ENNReal.ofReal_one])
    (fun x hx => by rw [multinomialReal_of_notMem hx, ENNReal.ofReal_zero])

Uses 4 · Used by 1

Statement usesMultinomial mass function · Nonnegativity of the multinomial mass function · Support of the multinomial mass lies in the antidiagonal · Normalization

Used byMass of the multinomial distribution at a count vector

TheoremMass of the multinomial distribution at a count vector#✓fully proved

The mass of the multinomial PMF at x is multinomialReal N p x.

theorem multinomial_apply {N : ℕ} {p : ι → ℝ} (hp₀ : ∀ i, 0 ≤ p i) (hp₁ : ∑ i, p i = 1)
    (x : ι → ℕ) : multinomial N p hp₀ hp₁ x = ENNReal.ofReal (multinomialReal N p x)

Uses 2

Statement usesMultinomial distribution as a probability mass function · Multinomial mass function

TheoremMean, polynomial form#✓fully proved

∑ₓ xᵢ P(x) = N pᵢ (∑ⱼ pⱼ) ^ (N - 1) for every real vector p.

theorem sum_mul_multinomialReal_eq (N : ℕ) (p : ι → ℝ) (i : ι) :
    ∑ x ∈ piAntidiag univ N, (x i : ℝ) * multinomialReal N p x =
      N * p i * (∑ j, p j) ^ (N - 1)

Uses 2 · Used by 3

Statement usesMultinomial mass function

Proof usesMultinomial theorem

Used bySecond factorial moment, polynomial form · Mean · Second factorial moment, polynomial form

TheoremSecond factorial moment, polynomial form#✓fully proved

For i ≠ j, ∑ₓ xᵢ xⱼ P(x) = N (N - 1) pᵢ pⱼ (∑ₗ pₗ) ^ (N - 2) for every real vector p.

theorem sum_mul_mul_multinomialReal_of_ne_eq (N : ℕ) (p : ι → ℝ) {i j : ι} (hij : i ≠ j) :
    ∑ x ∈ piAntidiag univ N, (x i : ℝ) * x j * multinomialReal N p x =
      N * (N - 1) * p i * p j * (∑ l, p l) ^ (N - 2)

Uses 2 · Used by 1

Statement usesMultinomial mass function

Proof usesMean, polynomial form

Used byMixed second moment

TheoremSecond factorial moment, polynomial form#✓fully proved

∑ₓ xᵢ (xᵢ - 1) P(x) = N (N - 1) pᵢ² (∑ₗ pₗ) ^ (N - 2) for every real vector p.

theorem sum_mul_sub_one_multinomialReal_eq (N : ℕ) (p : ι → ℝ) (i : ι) :
    ∑ x ∈ piAntidiag univ N, (x i : ℝ) * ((x i : ℝ) - 1) * multinomialReal N p x =
      N * (N - 1) * p i ^ 2 * (∑ l, p l) ^ (N - 2)

Uses 2 · Used by 1

Statement usesMultinomial mass function

Proof usesMean, polynomial form

Used bySecond factorial moment

TheoremMean#✓fully proved

For a probability vector (0 ≤ pᵢ, ∑ⱼ pⱼ = 1), E Xᵢ = N pᵢ. The underlying sum_mul_multinomialReal_eq is a polynomial identity holding for every real p.

theorem sum_mul_multinomialReal {N : ℕ} {p : ι → ℝ} (hp : ∑ i, p i = 1)
    (hp₀ : ∀ i, 0 ≤ p i) (i : ι) :
    ∑ x ∈ piAntidiag univ N, (x i : ℝ) * multinomialReal N p x = N * p i

Uses 2 · Used by 1

Statement usesMultinomial mass function

Proof usesMean, polynomial form

Used byCovariance

TheoremMixed second moment#✓fully proved

For a probability vector and i ≠ j, E[Xᵢ Xⱼ] = N (N - 1) pᵢ pⱼ.

theorem sum_mul_mul_multinomialReal_of_ne {N : ℕ} {p : ι → ℝ} (hp : ∑ i, p i = 1)
    (hp₀ : ∀ i, 0 ≤ p i) {i j : ι}
    (hij : i ≠ j) :
    ∑ x ∈ piAntidiag univ N, (x i : ℝ) * x j * multinomialReal N p x =
      N * (N - 1) * p i * p j

Uses 2 · Used by 1

Statement usesMultinomial mass function

Proof usesSecond factorial moment, polynomial form

Used byCovariance

TheoremSecond factorial moment#✓fully proved

For a probability vector, E[Xᵢ (Xᵢ - 1)] = N (N - 1) pᵢ².

theorem sum_mul_sub_one_multinomialReal {N : ℕ} {p : ι → ℝ} (hp : ∑ i, p i = 1)
    (hp₀ : ∀ i, 0 ≤ p i) (i : ι) :
    ∑ x ∈ piAntidiag univ N, (x i : ℝ) * ((x i : ℝ) - 1) * multinomialReal N p x =
      N * (N - 1) * p i ^ 2

Uses 2 · Used by 1

Statement usesMultinomial mass function

Proof usesSecond factorial moment, polynomial form

Used byCovariance

TheoremCovariance#✓fully proved

For a probability vector (0 ≤ pᵢ, ∑ₗ pₗ = 1), Cov(Xᵢ, Xⱼ) = ∑ₓ (xᵢ - N pᵢ) (xⱼ - N pⱼ) P(x) = N (δᵢⱼ pᵢ - pᵢ pⱼ); in particular Var Xᵢ = N pᵢ (1 - pᵢ) and Cov(Xᵢ, Xⱼ) = -N pᵢ pⱼ for i ≠ j.

theorem sum_covariance_multinomialReal {N : ℕ} {p : ι → ℝ} (hp : ∑ i, p i = 1)
    (hp₀ : ∀ i, 0 ≤ p i) (i j : ι) :
    ∑ x ∈ piAntidiag univ N,
        ((x i : ℝ) - N * p i) * ((x j : ℝ) - N * p j) * multinomialReal N p x =
      N * ((if i = j then p i else 0) - p i * p j)

Uses 5

Statement usesMultinomial mass function

Proof usesMixed second moment · Mean · Second factorial moment · Normalization

Poisson Conditioning

TheoremPoisson conditioning#✓fully proved

Let Xᵢ ~ Po(λᵢ), i ∈ ι, be independent Poisson counts with ∑ᵢ λᵢ > 0. Given their total ∑ᵢ Xᵢ = N, the count vector is multinomial with N throws and cell probabilities λᵢ / ∑ⱼ λⱼ: P(X = x | ∑ᵢ Xᵢ = N) = multinomialReal N (λ / ∑ λ) x.

theorem cond_measureReal_eq_multinomialReal {X : ι → Ω → ℕ} {r : ι → ℝ≥0}
    (hXm : ∀ i, Measurable (X i)) (hX : ∀ i, HasLaw (X i) (poissonMeasure (r i)) μ)
    (hind : iIndepFun X μ) (hr : 0 < ∑ i, r i) (N : ℕ) (x : ι → ℕ) :
    (μ[|{ω | ∑ i, X i ω = N}]).real {ω | ∀ i, X i ω = x i} =
      multinomialReal N (fun i => (r i : ℝ) / ∑ j, (r j : ℝ)) x

Uses 4

Statement usesMultinomial mass function

Proof usesMultinomial mass formula on the simplex · Multinomial mass vanishes off the simplex · Multinomial theorem

TheoremPoisson conditioning, two cells#✓fully proved

For independent X ~ Po(a) and Y ~ Po(b) with a + b > 0, the law of X given X + Y = N is binomial Bin(N, a / (a + b)).

theorem cond_measureReal_eq_binomial {X Y : Ω → ℕ} {a b : ℝ≥0} (hab : 0 < a + b)
    (hXm : Measurable X) (hYm : Measurable Y) (hX : HasLaw X (poissonMeasure a) μ)
    (hY : HasLaw Y (poissonMeasure b) μ) (hXY : IndepFun X Y μ) (N k : ℕ) :
    (μ[|{ω | X ω + Y ω = N}]).real {ω | X ω = k} =
      (binomial N ⟨(a : ℝ) / (a + b), div_nonneg a.2 (add_nonneg a.2 b.2),
        div_le_one_of_le₀ (le_add_of_nonneg_right b.2) (add_nonneg a.2 b.2)⟩).real {k}

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.