Aggregation pushforward of simplex coordinate measure

noncomputable def MeasureTheory.Measure.stdSimplexAggregateDensity {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] (f : ι → κ) (v : κ → ℝ) : ENNReal

Density associated with the cardinalities of the fibers of a coordinate aggregation map.

Equations

• MeasureTheory.Measure.stdSimplexAggregateDensity f v = ∏ k : κ, ENNReal.ofReal (v k) ^ (stdSimplexAggregateFiberCard f k - 1) / ↑(stdSimplexAggregateFiberCard f k - 1).factorial

theorem MeasureTheory.Measure.sum_stdSimplexAggregateFiberCard_sub_one {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] {f : ι → κ} (hf : Function.Surjective f) : ∑ k : κ, (stdSimplexAggregateFiberCard f k - 1) = Fintype.card ι - Fintype.card κ

For a surjective aggregation, the total degree of the aggregation density is the difference between the dimensions of the source and target affine coordinate spaces.

theorem MeasureTheory.Measure.map_stdSimplexMeasure_restrict_stdSimplex_aggregate_of_unique {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] [Unique κ] [Nonempty ι] (f : ι → κ) : map (stdSimplexAggregate f) (stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ ι)) = (stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ κ)).withDensity (stdSimplexAggregateDensity f)

The aggregation formula when the target has one coordinate. This is the base case for fiberwise induction on a general surjective aggregation map.

theorem MeasureTheory.Measure.map_stdSimplexMeasure_restrict_stdSimplex_aggregate {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] (f : ι → κ) (hf : Function.Surjective f) : map (stdSimplexAggregate f) (stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ ι)) = (stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ κ)).withDensity (stdSimplexAggregateDensity f)

Pushing the restricted simplex measure forward under coordinate aggregation gives the restricted target simplex measure weighted by the product of the fiber-volume densities.

This is the standard-simplex form of lintegral_posSimplex_comp_aggregate.