Transforms of the multinomial distribution

For the pushforward of multinomialMeasure n p into EuclideanSpace ℝ ι along multinomialToEuclidean and a direction θ, the directional moment generating function is finite everywhere and equals (∑ i, p i * exp (t * θ i)) ^ n: the multinomial theorem, with the cell weights tilted by exp (t * θ i). The cumulant generating function is its real logarithm.

The characteristic function of the Euclidean cast is the corresponding complex multinomial polynomial, (∑ i, p i * exp (I * t i)) ^ n.

A probability vector on ι forces ι to be nonempty, so the statements need no separate hypothesis for it beyond the parameter p. Every statement holds for n = 0 (the law is a Dirac mass at zero, and the formula is 1) and for probability vectors with zero cells, which contribute nothing to the tilted sum.

Main results

• TauCeti.Probability.integrableExpSet_multinomialMeasure — every real observable has full exponential integrability domain, and TauCeti.Probability.integrableExpSet_inner_multinomial for every direction of the Euclidean pushforward;
• TauCeti.Probability.mgf_inner_multinomial — the directional moment generating function;
• TauCeti.Probability.cgf_inner_multinomial — the directional cumulant generating function.
• TauCeti.Probability.charFun_map_multinomialToEuclidean_multinomialMeasure — the characteristic function of the Euclidean cast.

References

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

theorem TauCeti.Probability.mgf_inner_multinomial {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) (θ : EuclideanSpace ℝ ι) (t : ℝ) : ProbabilityTheory.mgf (fun (x : EuclideanSpace ℝ ι) => inner ℝ θ x) (MeasureTheory.Measure.map multinomialToEuclidean (multinomialMeasure n p)) t = (∑ i : ι, ↑(p.weights i) * Real.exp (t * θ.ofLp i)) ^ n

Directional moment generating function of the multinomial law: for every direction θ and every t, it is (∑ i, pᵢ exp (t θᵢ)) ^ n.

theorem TauCeti.Probability.integrableExpSet_multinomialMeasure {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) (f : (ι → ℕ) → ℝ) : ProbabilityTheory.integrableExpSet f (multinomialMeasure n p) = Set.univ

Every real observable of a multinomial law has full exponential-integrability domain: the law has finite support.

theorem TauCeti.Probability.integrableExpSet_inner_multinomial {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) (θ : EuclideanSpace ℝ ι) : ProbabilityTheory.integrableExpSet (fun (x : EuclideanSpace ℝ ι) => inner ℝ θ x) (MeasureTheory.Measure.map multinomialToEuclidean (multinomialMeasure n p)) = Set.univ

Every direction has full exponential-integrability domain for the Euclidean pushforward.

theorem TauCeti.Probability.cgf_inner_multinomial {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) (θ : EuclideanSpace ℝ ι) (t : ℝ) : ProbabilityTheory.cgf (fun (x : EuclideanSpace ℝ ι) => inner ℝ θ x) (MeasureTheory.Measure.map multinomialToEuclidean (multinomialMeasure n p)) t = Real.log ((∑ i : ι, ↑(p.weights i) * Real.exp (t * θ.ofLp i)) ^ n)

Directional cumulant generating function of the multinomial law: the real logarithm of the moment generating function.

theorem TauCeti.Probability.charFun_map_multinomialToEuclidean_multinomialMeasure {ι : Type u_1} [Fintype ι] (n : ℕ) (p : Convexity.StdSimplex NNReal ι) (t : EuclideanSpace ℝ ι) : MeasureTheory.charFun (MeasureTheory.Measure.map multinomialToEuclidean (multinomialMeasure n p)) t = (∑ i : ι, ↑↑(p.weights i) * Complex.exp (Complex.I * ↑(t.ofLp i))) ^ n

Characteristic function of the multinomial law: for a frequency vector t, it is the nth power of the probability-weighted sum of the coordinate characters.