Parameter measurability of the multinomial distribution #
The multinomial law is a measurable function of its parameters, the sample size n : ℕ and the
probability vector p : StdSimplex ℝ≥0 ι, the simplex carrying the σ-algebra induced by its
weight vector. This is what lets the multinomial law be used with random parameters: it is a
measurable map into the Giry space, hence a kernel from the parameter space.
Main results #
TauCeti.Probability.measurable_multinomialWeight— each multinomial weight is a measurable function of the weight vector;TauCeti.Probability.measurable_multinomialMeasure— the law is a measurable function of the sample size and the probability vector jointly.
theorem
TauCeti.Probability.measurable_multinomialWeight
{ι : Type u_1}
[Fintype ι]
(k : ι → ℕ)
:
Measurable fun (w : ι → NNReal) => multinomialWeight w k
Each multinomial weight is a measurable function of the weight vector.
theorem
TauCeti.Probability.measurable_multinomialMeasure
{ι : Type u_1}
[Fintype ι]
:
Measurable fun (q : ℕ × Convexity.StdSimplex NNReal ι) => multinomialMeasure q.1 q.2
Parameter measurability of the multinomial law: it is a measurable function of the sample size and the probability vector jointly.