The multinomial distribution

For a natural number n and a probability vector p, the multinomial distribution assigns to a count vector k of total size n the mass

  multinomial(univ, k) * ∏ i, p.weights i ^ k i.

This file defines the distribution as a finite weighted sum of Dirac measures and establishes its normalization, exact singleton masses and support, and finite-sum integration formula. The parameter space is Mathlib's Convexity.StdSimplex ℝ≥0 ι; its weights are nonnegative real numbers summing to one.

Main definitions and results

• TauCeti.Probability.multinomialWeightReal: the real-valued multinomial weight.
• TauCeti.Probability.multinomialWeight: the extended nonnegative multinomial weight.
• TauCeti.Probability.multinomialMeasure: the multinomial measure on count vectors.
• TauCeti.Probability.isProbabilityMeasure_multinomialMeasure: normalization.
• TauCeti.Probability.multinomialMeasure_singleton: the exact singleton mass.
• TauCeti.Probability.multinomialMeasure_singleton_ne_zero_iff: the exact support.
• TauCeti.Probability.integral_multinomialMeasure: integration as a finite weighted sum.
• TauCeti.Probability.multinomialToEuclidean: the cast of count vectors into Euclidean space, the carrier of the law's mean, covariance and transforms.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Discrete Multivariate Distributions, Wiley, 1997, Chapter 35.

def TauCeti.Probability.multinomialWeightReal {ι : Type u_1} [Fintype ι] (w : ι → NNReal) (k : ι → ℕ) : ℝ

The real-valued multinomial weight associated to nonnegative cell weights.

It is indexed by cell weights w and a count vector k. The weights need not sum to one; the multinomial measure specializes them to the weights of a probability vector.

theorem TauCeti.Probability.multinomialWeightReal_def {ι : Type u_1} [Fintype ι] (w : ι → NNReal) (k : ι → ℕ) : multinomialWeightReal w k = ↑(Nat.multinomial Finset.univ k) * ∏ i : ι, ↑(w i) ^ k i

The defining formula of the real multinomial weight, for use across module boundaries.

theorem TauCeti.Probability.multinomialWeightReal_nonneg {ι : Type u_1} [Fintype ι] (w : ι → NNReal) (k : ι → ℕ) : 0 ≤ multinomialWeightReal w k

Every real multinomial weight is nonnegative.

noncomputable def TauCeti.Probability.multinomialWeight {ι : Type u_1} [Fintype ι] (w : ι → NNReal) (k : ι → ℕ) : ENNReal

The ℝ≥0∞-valued multinomial weight used to scale Dirac measures.

theorem TauCeti.Probability.multinomialWeight_def {ι : Type u_1} [Fintype ι] (w : ι → NNReal) (k : ι → ℕ) : multinomialWeight w k = ↑(Nat.multinomial Finset.univ k) * ∏ i : ι, ↑(w i) ^ k i

The extended nonnegative multinomial weight in terms of the multinomial coefficient and cell weights.

@[simp]

theorem TauCeti.Probability.multinomialWeight_toReal {ι : Type u_1} [Fintype ι] (w : ι → NNReal) (k : ι → ℕ) : (multinomialWeight w k).toReal = multinomialWeightReal w k

The extended nonnegative multinomial weight has the expected real value.

noncomputable def TauCeti.Probability.multinomialMeasure {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) : MeasureTheory.Measure (ι → ℕ)

The multinomial distribution with sample size n and cell probabilities p.

The finite antidiagonal consists precisely of the count vectors whose coordinates sum to n.

theorem TauCeti.Probability.multinomialMeasure_def {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) : multinomialMeasure n p = ∑ k ∈ Finset.univ.piAntidiag n, multinomialWeight (⇑p.weights) k • MeasureTheory.Measure.dirac k

The multinomial measure as its defining finite weighted sum of Dirac measures.

theorem TauCeti.Probability.sum_multinomialWeightReal {ι : Type u_1} [Fintype ι] (n : ℕ) (w : ι → NNReal) : ∑ k ∈ Finset.univ.piAntidiag n, multinomialWeightReal w k = (∑ i : ι, ↑(w i)) ^ n

The real multinomial weights on a fixed antidiagonal satisfy the multinomial theorem.

theorem TauCeti.Probability.sum_multinomialWeightReal_eq_one {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) : ∑ k ∈ Finset.univ.piAntidiag n, multinomialWeightReal (⇑p.weights) k = 1

The real multinomial weights of a probability vector sum to one.

theorem TauCeti.Probability.sum_multinomialWeight {ι : Type u_1} [Fintype ι] (n : ℕ) (w : ι → NNReal) : ∑ k ∈ Finset.univ.piAntidiag n, multinomialWeight w k = (∑ i : ι, ↑(w i)) ^ n

The ℝ≥0∞-valued multinomial weights satisfy the multinomial theorem.

theorem TauCeti.Probability.sum_multinomialWeight_eq_one {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) : ∑ k ∈ Finset.univ.piAntidiag n, multinomialWeight (⇑p.weights) k = 1

The ℝ≥0∞-valued multinomial weights of a probability vector sum to one.

theorem TauCeti.Probability.isProbabilityMeasure_multinomialMeasure {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) : MeasureTheory.IsProbabilityMeasure (multinomialMeasure n p)

The multinomial law is a probability measure.

@[simp]

theorem TauCeti.Probability.multinomialMeasure_zero {ι : Type u_1} [Fintype ι] (p : Convexity.StdSimplex NNReal ι) : multinomialMeasure 0 p = MeasureTheory.Measure.dirac 0

With no trials, the multinomial law is concentrated at the zero count vector.

@[simp]

theorem TauCeti.Probability.multinomialMeasure_singleton {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) (k : ι → ℕ) : (multinomialMeasure n p) {k} = if ∑ i : ι, k i = n then multinomialWeight (⇑p.weights) k else 0

The singleton mass of a multinomial law is its defining weight on the count antidiagonal and zero elsewhere.

@[simp]

theorem TauCeti.Probability.multinomialMeasure_real_singleton {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) (k : ι → ℕ) : (multinomialMeasure n p).real {k} = if ∑ i : ι, k i = n then (↑n.factorial / ∏ i : ι, ↑(k i).factorial) * ∏ i : ι, ↑(p.weights i) ^ k i else 0

The real singleton mass of a multinomial law, in the usual factorial form.

@[simp]

theorem TauCeti.Probability.multinomialWeight_ne_zero_iff {ι : Type u_1} [Fintype ι] (w : ι → NNReal) (k : ι → ℕ) : multinomialWeight w k ≠ 0 ↔ ∀ (i : ι), k i ≠ 0 → w i ≠ 0

A multinomial weight is nonzero exactly when every cell receiving a positive count has positive weight.

theorem TauCeti.Probability.multinomialMeasure_singleton_ne_zero_iff {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) (k : ι → ℕ) : (multinomialMeasure n p) {k} ≠ 0 ↔ ∑ i : ι, k i = n ∧ ∀ (i : ι), k i ≠ 0 → p.weights i ≠ 0

The singleton mass is nonzero precisely for count vectors of total size n which do not use a zero-weight cell.

@[simp]

theorem TauCeti.Probability.multinomialWeight_ne_top {ι : Type u_1} [Fintype ι] (w : ι → NNReal) (k : ι → ℕ) : multinomialWeight w k ≠ ⊤

Every multinomial weight is finite.

@[simp]

theorem TauCeti.Probability.multinomialMeasure_sum_eq {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) : (multinomialMeasure n p) {k : ι → ℕ | ∑ i : ι, k i = n} = 1

A multinomial law is concentrated on count vectors whose coordinates sum to the sample size.

theorem TauCeti.Probability.integrable_multinomialMeasure {ι : Type u_1} [Fintype ι] {E : Type u_2} [SeminormedAddGroup E] (f : (ι → ℕ) → E) (n : ℕ) (p : Convexity.StdSimplex NNReal ι) : MeasureTheory.Integrable f (multinomialMeasure n p)

Every function is integrable against a multinomial law because the law has finite support.

theorem TauCeti.Probability.integral_multinomialMeasure {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : (ι → ℕ) → E) (n : ℕ) (p : Convexity.StdSimplex NNReal ι) : ∫ (k : ι → ℕ), f k ∂multinomialMeasure n p = ∑ k ∈ Finset.univ.piAntidiag n, multinomialWeightReal (⇑p.weights) k • f k

Integration against a multinomial law is the corresponding finite weighted sum.

noncomputable def TauCeti.Probability.multinomialToEuclidean {ι : Type u_1} (k : ι → ℕ) : EuclideanSpace ℝ ι

The count vector cast into Euclidean space.

@[simp]

theorem TauCeti.Probability.multinomialToEuclidean_apply {ι : Type u_1} (k : ι → ℕ) (i : ι) : (multinomialToEuclidean k).ofLp i = ↑(k i)

The coordinates of the cast are the counts, as reals.

theorem TauCeti.Probability.inner_multinomialToEuclidean {ι : Type u_1} [Fintype ι] (θ : EuclideanSpace ℝ ι) (k : ι → ℕ) : inner ℝ θ (multinomialToEuclidean k) = ∑ i : ι, θ.ofLp i * ↑(k i)

Pairing a direction with the Euclidean count vector is the corresponding weighted sum.

theorem TauCeti.Probability.measurable_multinomialToEuclidean {ι : Type u_1} : Measurable multinomialToEuclidean

The cast of count vectors into Euclidean space is measurable.

theorem TauCeti.Probability.isClosedEmbedding_multinomialToEuclidean {ι : Type u_1} : Topology.IsClosedEmbedding multinomialToEuclidean

Casting count vectors into Euclidean space is a closed embedding. In particular, closed sets of count vectors remain closed after casting, even when they are infinite.

theorem TauCeti.Probability.measurableEmbedding_multinomialToEuclidean {ι : Type u_1} [Finite ι] : MeasurableEmbedding multinomialToEuclidean

Casting count vectors into Euclidean space is a measurable embedding.