Basic integration with the affine-hyperplane coordinate measure

theorem MeasureTheory.integral_smul_free_coords {ι : Type u} [Fintype ι] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i : ι) (c : ℝ) (hc : 0 < c) (f : ({ j : ι // j ≠ i } → ℝ) → E) : ∫ (x : { j : ι // j ≠ i } → ℝ), f (c • x) = (c ^ (Fintype.card ι - 1))⁻¹ • ∫ (x : { j : ι // j ≠ i } → ℝ), f x

Scaling the free coordinates by c divides the Bochner integral by c ^ (card ι - 1).

theorem MeasureTheory.integral_stdSimplex_eq_integral_freeCoords {ι : Type u} [Fintype ι] [Nonempty ι] (i : ι) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ) → E) : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f u ∂Measure.stdSimplexMeasure = ∫ (x : { j : ι // j ≠ i } → ℝ) in stdSimplexFreeCoords i, f (stdSimplexCoordMap i x)

Integration over the standard simplex can be computed in any free-coordinate chart. This is stated for functions taking values in a normed real vector space.

theorem MeasureTheory.lintegral_stdSimplex_eq_lintegral_freeCoords {ι : Type u} [Fintype ι] [Nonempty ι] (i : ι) (f : (ι → ℝ) → ENNReal) : ∫⁻ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f u ∂Measure.stdSimplexMeasure = ∫⁻ (x : { j : ι // j ≠ i } → ℝ) in stdSimplexFreeCoords i, f (stdSimplexCoordMap i x)

A nonnegative integral over the standard simplex can be computed in any free-coordinate chart.

theorem MeasureTheory.integral_stdSimplex_comp_perm {ι : Type u} [Fintype ι] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (σ : Equiv.Perm ι) (f : (ι → ℝ) → E) : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f (u ∘ ⇑σ) ∂Measure.stdSimplexMeasure = ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f u ∂Measure.stdSimplexMeasure

The integral of a function over the standard simplex is invariant under coordinate permutations.

theorem MeasureTheory.ContinuousOn.integrableOn_stdSimplex {ι : Type u} [Fintype ι] {E : Type u_1} [NormedAddCommGroup E] {f : (ι → ℝ) → E} (hf : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)) : IntegrableOn f (Convexity.StdSimplex.coordinateSet ℝ ι) Measure.stdSimplexMeasure

Continuous functions are integrable on the standard simplex.

theorem MeasureTheory.integral_stdSimplex_congr {ι : Type u} [Fintype ι] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : (ι → ℝ) → E} (hfg : Set.EqOn f g (Convexity.StdSimplex.coordinateSet ℝ ι)) : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f u ∂Measure.stdSimplexMeasure = ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, g u ∂Measure.stdSimplexMeasure

The integral of f over the standard simplex depends only on the values of f on the standard simplex.

theorem MeasureTheory.integral_stdSimplex_unique {ι : Type u} [Fintype ι] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [Unique ι] (f : (ι → ℝ) → E) : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f u ∂Measure.stdSimplexMeasure = f fun (x : ι) => 1

For a single-point index set, the integral over the simplex reduces to evaluation at the all-ones vector. (Base case for induction.)