Finite-coordinate simplex integrals

The last barycentric coordinate is reconstructed from the other coordinates. Separating the last free coordinate gives the one-dimensional slices used by the simplex FTC.

def MeasureTheory.finSimplexPoint {n : ℕ} (v : Fin n → ℝ) : Fin (n + 1) → ℝ

Reconstruct the last barycentric coordinate.

Equations

• MeasureTheory.finSimplexPoint v = Fin.snoc v (1 - ∑ k : Fin n, v k)

theorem MeasureTheory.continuous_finSimplexPoint {n : ℕ} : Continuous finSimplexPoint

theorem MeasureTheory.finSimplexPoint_mem {n : ℕ} {v : Fin n → ℝ} (hv : v ∈ posSimplexFin n 1) : finSimplexPoint v ∈ Convexity.StdSimplex.coordinateSet ℝ (Fin (n + 1))

theorem MeasureTheory.isCompact_posSimplexFin_one (n : ℕ) : IsCompact (posSimplexFin n 1)

theorem MeasureTheory.integral_stdSimplex_fin {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : (Fin (n + 1) → ℝ) → E) : ∫ (u : Fin (n + 1) → ℝ) in Convexity.StdSimplex.coordinateSet ℝ (Fin (n + 1)), g u ∂Measure.stdSimplexMeasure = ∫ (v : Fin n → ℝ) in posSimplexFin n 1, g (finSimplexPoint v)

The standard-simplex integral in the chart omitting its last coordinate.

theorem MeasureTheory.integral_posSimplexFin_snoc {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : (Fin (n + 1) → ℝ) → E) (hg : IntegrableOn g (posSimplexFin (n + 1) 1) volume) : ∫ (v : Fin (n + 1) → ℝ) in posSimplexFin (n + 1) 1, g v = ∫ (v : Fin n → ℝ) in posSimplexFin n 1, ∫ (t : ℝ) in Set.Icc 0 (1 - ∑ k : Fin n, v k), g (Fin.snoc v t)

Fubini with the last free coordinate integrated first.

theorem MeasureTheory.integral_posSimplexFin_snoc_outer {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : (Fin (n + 1) → ℝ) → E) (hg : IntegrableOn g (posSimplexFin (n + 1) 1) volume) : ∫ (v : Fin (n + 1) → ℝ) in posSimplexFin (n + 1) 1, g v = ∫ (t : ℝ) in Set.Icc 0 1, ∫ (v : Fin n → ℝ) in posSimplexFin n (1 - t), g (Fin.snoc v t)

The same Fubini decomposition, with the separated coordinate integrated last.

theorem MeasureTheory.integral_posSimplexFin_scale {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : (Fin n → ℝ) → E) {r : ℝ} (hr : 0 < r) : ∫ (v : Fin n → ℝ) in posSimplexFin n r, g v = r ^ n • ∫ (v : Fin n → ℝ) in posSimplexFin n 1, g (r • v)

Dilation of the solid simplex.