Aggregation of the real Dirichlet distribution

theorem ProbabilityTheory.mem_mvRealBetaDomain_stdSimplexAggregate {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Finite κ] {f : ι → κ} (hf : Function.Surjective f) {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : stdSimplexAggregate f b ∈ mvRealBetaDomain

Aggregating a Dirichlet parameter vector along a surjection stays in the positive parameter domain.

theorem ProbabilityTheory.continuous_stdSimplexAggregate {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Finite κ] (f : ι → κ) : Continuous (stdSimplexAggregate f)

Coordinate aggregation is continuous, as a linear map on a finite product.

theorem ProbabilityTheory.integral_dirichletMeasure_comp_stdSimplexAggregate_monomial {ι : Type u_1} [Fintype ι] [Nonempty ι] {κ : Type u_2} [Fintype κ] {f : ι → κ} (hf : Function.Surjective f) {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (m : κ → ℕ) : ∫ (u : ι → ℝ), ∏ k : κ, stdSimplexAggregate f u k ^ m k ∂dirichletMeasure b = ∫ (v : κ → ℝ), ∏ k : κ, v k ^ m k ∂dirichletMeasure (stdSimplexAggregate f b)

Pushing a Dirichlet monomial forward under coordinate aggregation yields the Dirichlet monomial for the aggregated parameters. This is the moment form of the multinomial Chu–Vandermonde identity.

theorem ProbabilityTheory.measurePreserving_stdSimplexAggregate_dirichletMeasure {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] {f : ι → κ} (hf : Function.Surjective f) {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : MeasureTheory.MeasurePreserving (stdSimplexAggregate f) (dirichletMeasure b) (dirichletMeasure (stdSimplexAggregate f b))

Dirichlet measure is closed under marginalisation or coarsening: pushing dirichletMeasure b forward along stdSimplexAggregate f gives the Dirichlet measure for the aggregated parameter vector.

theorem ProbabilityTheory.stdSimplexAggregate_withDensity {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] {f : ι → κ} (hf : Function.Surjective f) {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : MeasureTheory.Measure.map (stdSimplexAggregate f) (MeasureTheory.Measure.stdSimplexMeasure.withDensity fun (u : ι → ℝ) => ENNReal.ofReal (dirichletPdfReal b u)) = MeasureTheory.Measure.stdSimplexMeasure.withDensity fun (v : κ → ℝ) => ENNReal.ofReal (dirichletPdfReal (stdSimplexAggregate f b) v)

Coordinate aggregation restated via the explicit density, unfolding measurePreserving_stdSimplexAggregate_dirichletMeasure in terms of stdSimplexMeasure and dirichletPdf directly rather than the bundled dirichletMeasure.