Integrals over the standard simplex

Let Δᵖ⁺¹ = {x ∈ ℝᵖ⁺¹ | 0 ≤ xᵢ, ∑ xᵢ ≤ 1} be the full-dimensional standard simplex. Slicing it along its j-th coordinate writes an integral over Δᵖ⁺¹ as an iterated integral over 0 ≤ x_j ≤ 1 - ∑_{i ≠ j} xᵢ and then over the remaining coordinates in Δᵖ. Combined with the fundamental theorem of calculus on each slice, this computes the integral over Δᵖ⁺¹ of a partial derivative of a C¹ function as the difference of its integrals over the face ∑ xᵢ = 1 and the face x_j = 0. The face ∑ xᵢ = 1 read through the coordinates other than the j-th one, and read through the face map simplexMapAmbient (Fin.succAbove 0), differ by an affine symmetry of Δᵖ permuting its vertices, so integrals over the two readings agree.

These are the scalar computations behind Stokes' theorem on the standard simplex.

Main results

• TauCeti.setIntegral_fullSimplex_eq_iterated: the integral over Δᵖ⁺¹ of a function integrable on it, as an iterated integral along the j-th coordinate and then over Δᵖ.
• ContDiffOn.integral_fderivWithin_fullSimplex: the integral over Δᵖ⁺¹ of the j-th partial derivative of a C¹ function is the difference of its integrals over the face ∑ xᵢ = 1 and the face xⱼ = 0, both read through the coordinates other than the j-th one.
• TauCeti.setIntegral_toLp_insertNth_eq: the two readings of the face ∑ xᵢ = 1 give the same integral.

theorem TauCeti.setIntegral_fullSimplex_eq_iterated {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ℕ} {D : EuclideanSpace ℝ (Fin (p + 1)) → F} (hD : MeasureTheory.IntegrableOn D (fullSimplex (p + 1)) MeasureTheory.volume) (j : Fin (p + 1)) : ∫ (x : EuclideanSpace ℝ (Fin (p + 1))) in fullSimplex (p + 1), D x = ∫ (y : Fin p → ℝ) in coordinateSimplex (Fin p), ∫ (t : ℝ) in Set.Icc 0 (1 - ∑ k : Fin p, y k), D (WithLp.toLp 2 (j.insertNth t y))

Slicing the standard simplex along a coordinate. The integral over Δᵖ⁺¹ of a function integrable on it is the iterated integral that first integrates along the j-th coordinate, over 0 ≤ t ≤ 1 - ∑ k, y k, and then over the remaining coordinates y in the coordinate simplex.

theorem ContDiffOn.integral_fderivWithin_fullSimplex {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {p : ℕ} {g : EuclideanSpace ℝ (Fin (p + 1)) → F} (hg : ContDiffOn ℝ 1 g (TauCeti.fullSimplex (p + 1))) (j : Fin (p + 1)) : ∫ (x : EuclideanSpace ℝ (Fin (p + 1))) in TauCeti.fullSimplex (p + 1), (fderivWithin ℝ g (TauCeti.fullSimplex (p + 1)) x) (EuclideanSpace.single j 1) = ∫ (y : EuclideanSpace ℝ (Fin p)) in TauCeti.fullSimplex p, g (WithLp.toLp 2 (j.insertNth (1 - ∑ k : Fin p, y.ofLp k) y.ofLp)) - g (WithLp.toLp 2 (j.insertNth 0 y.ofLp))

The fundamental theorem of calculus along a coordinate of the standard simplex. For a function g that is C¹ on Δᵖ⁺¹, the integral over Δᵖ⁺¹ of its partial derivative in the direction e_j is the integral over Δᵖ of the difference of its values at the points of the faces ∑ xᵢ = 1 and x_j = 0 whose other coordinates are given by y ∈ Δᵖ.

theorem TauCeti.setIntegral_toLp_insertNth_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {p : ℕ} (j : Fin (p + 1)) (G : EuclideanSpace ℝ (Fin (p + 1)) → F) : ∫ (y : EuclideanSpace ℝ (Fin p)) in fullSimplex p, G (WithLp.toLp 2 (j.insertNth (1 - ∑ k : Fin p, y.ofLp k) y.ofLp)) = ∫ (y : EuclideanSpace ℝ (Fin p)) in fullSimplex p, G ((simplexMapAmbient (Fin.succAbove 0)) y)

Reading the face of Δᵖ⁺¹ opposite the origin through the coordinates other than the j-th one, or through the last p coordinates, gives the same integral.