Coordinate aggregation in standard-simplex integrals

theorem MeasureTheory.integral_stdSimplex_comp_aggregate {ι : Type u} [Fintype ι] {κ : Type u_1} [Fintype κ] (f : ι → κ) (hf : Function.Surjective f) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : (κ → ℝ) → E) (hg : AEStronglyMeasurable g ((Measure.stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ κ)).withDensity (Measure.stdSimplexAggregateDensity f))) : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, g (stdSimplexAggregate f u) ∂Measure.stdSimplexMeasure = ∫ (v : κ → ℝ) in Convexity.StdSimplex.coordinateSet ℝ κ, (∏ k : κ, v k ^ (stdSimplexAggregateFiberCard f k - 1) / ↑(stdSimplexAggregateFiberCard f k - 1).factorial) • g v ∂Measure.stdSimplexMeasure

Transformation of integrals under coordinate aggregation. The measurability hypothesis is stated for the weighted target measure, which is exactly the push-forward measure occurring in the change of variables.