Solid simplex integration by coordinate sum

theorem lintegral_Icc_triangle_swap (r : ℝ) (_hr : 0 ≤ r) (F : ℝ → ℝ → ENNReal) (hF : Measurable (Function.uncurry F)) : ∫⁻ (t : ℝ) in Set.Icc 0 r, ∫⁻ (s : ℝ) in Set.Icc t r, F t s = ∫⁻ (s : ℝ) in Set.Icc 0 r, ∫⁻ (t : ℝ) in Set.Icc 0 s, F t s

Tonelli's theorem on the triangle 0 ≤ t ≤ s ≤ r.

theorem lintegral_posSimplexFin_comp_sum (n : ℕ) (hn : 0 < n) (r : ℝ) (hr : 0 ≤ r) (g : ℝ → ENNReal) (hg : Measurable g) : ∫⁻ (x : Fin n → ℝ) in posSimplexFin n r, g (∑ i : Fin n, x i) = ∫⁻ (s : ℝ) in Set.Icc 0 r, g s * (ENNReal.ofReal s ^ (n - 1) / ↑(n - 1).factorial)

Pushing the positive Fin n-simplex forward under the coordinate-sum map.

theorem lintegral_posSimplex_comp_sum {α : Type u_1} [Fintype α] [Nonempty α] (r : ℝ) (hr : 0 ≤ r) (g : ℝ → ENNReal) (hg : Measurable g) : ∫⁻ (x : α → ℝ) in posSimplex α r, g (∑ i : α, x i) = ∫⁻ (s : ℝ) in Set.Icc 0 r, g s * (ENNReal.ofReal s ^ (Fintype.card α - 1) / ↑(Fintype.card α - 1).factorial)

Pushing an arbitrary finite-dimensional positive simplex forward under the coordinate-sum map. Requires a nonempty index type so that the exponent card α - 1 is well-defined.