Monomial and polynomial integrals on the standard simplex

theorem MeasureTheory.integral_stdSimplex_explicit_monomial_succ {ι : Type u} [Fintype ι] [Nontrivial ι] (i : ι) (m : ι → ℕ) : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, ∏ j : ι, u j ^ m j ∂Measure.stdSimplexMeasure = ↑(m i).factorial * ↑(Fintype.card ι + ∑ j : ι, m j - 2 - m i).factorial / ↑(Fintype.card ι + ∑ j : ι, m j - 1).factorial * ∫ (u : { j : ι // j ≠ i } → ℝ) in Convexity.StdSimplex.coordinateSet ℝ { j : ι // j ≠ i }, ∏ j : { j : ι // j ≠ i }, u j ^ m ↑j ∂Measure.stdSimplexMeasure

Reduce a monomial integral on a nontrivial simplex to the monomial integral on the simplex obtained by deleting coordinate i.

theorem MeasureTheory.integral_stdSimplex_explicit_monomial {ι : Type u} [Fintype ι] (m : ι → ℕ) [Nonempty ι] : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, ∏ i : ι, u i ^ m i ∂Measure.stdSimplexMeasure = ↑(∏ i : ι, (m i).factorial) / ↑(Fintype.card ι + ∑ i : ι, m i - 1).factorial

The integral of a monomial with natural exponents over the standard simplex.

theorem MeasureTheory.integral_stdSimplex_constant {ι : Type u} [Fintype ι] [Nonempty ι] : ∫ (x : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, 1 ∂Measure.stdSimplexMeasure = 1 / ↑(Fintype.card ι - 1).factorial

The integral of the constant function 1 over the standard simplex.

theorem MeasureTheory.integral_stdSimplex_MvPolynomial_monomial {ι : Type u} [Fintype ι] (m : ι →₀ ℕ) [Nonempty ι] : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, m.prod fun (i : ι) (n : ℕ) => u i ^ n ∂Measure.stdSimplexMeasure = ↑(∏ i : ι, (m i).factorial) / ↑(Fintype.card ι + ∑ i : ι, m i - 1).factorial

The integral of a MvPolynomial monomial over the standard simplex.