Coordinates of the standard-simplex centroid

Coordinate permutations preserve both Euclidean volume and the standard simplex. Hence all centroid coordinates agree; their value follows from the already computed coordinate sum.

theorem Grunbaum.simplexSet_image_piLpCongrLeft (n : ℕ) (σ : Equiv.Perm (Fin n)) : ⇑(LinearIsometryEquiv.piLpCongrLeft 2 ℝ ℝ σ) '' simplexSet n = simplexSet n

theorem Grunbaum.integral_simplex_coordinate_eq (n : ℕ) (i j : Fin n) : ∫ (x : SimplexE n) in simplexSet n, x.ofLp i = ∫ (x : SimplexE n) in simplexSet n, x.ofLp j

theorem Grunbaum.simplexCentroid_coordinate_eq (n : ℕ) (i j : Fin n) : (simplexCentroid n).ofLp i = (simplexCentroid n).ofLp j

theorem Grunbaum.simplexCentroid_apply (n : ℕ) (i : Fin n) : (simplexCentroid n).ofLp i = (↑n + 1)⁻¹

Every coordinate of the volume centroid of the standard n-simplex equals 1 / (n + 1).