Weights of affine simplices in a standard simplex

A point w of a standard simplex on a finite type N is determined by its weight vector ⇑w.weights : N → ℝ, and Mathlib's topology on StdSimplex ℝ N is the one induced by this embedding (Convexity.StdSimplex.isEmbedding_toFun_comp_weights). This file computes the weight vectors of the points of the affine simplex Convexity.StdSimplex.affineMapMk v with vertices v m:

• Convexity.StdSimplex.weights_affineMapMk_subBarycenter: the image of the barycenter of the face spanned by S has as weight vector the centroid of the weight vectors of the vertices v m, m ∈ S;
• Convexity.StdSimplex.dist_weights_affineMapMk_le: every point of the affine simplex lies in each closed ball, for the sup metric on weight vectors, containing all of its vertices.

These are the metric facts about affine simplices used to show that iterated barycentric subdivision produces arbitrarily small simplices.

theorem Convexity.StdSimplex.weights_affineMapMk_subBarycenter {M : Type u_1} {N : Type u_2} [Finite M] (v : M → StdSimplex ℝ N) (S : Finset M) (hS : S.Nonempty) : ⇑((affineMapMk v) (subBarycenter S hS)).weights = Finset.centroid ℝ S fun (m : M) => ⇑(v m).weights

The image under the affine map with vertices v of the barycenter of the face spanned by S has as weight vector the centroid of the weight vectors of the vertices v m, m ∈ S.

theorem Convexity.StdSimplex.dist_weights_affineMapMk_le {M : Type u_1} {N : Type u_2} [Finite M] [Fintype N] (v : M → StdSimplex ℝ N) {q : N → ℝ} {r : ℝ} (h : ∀ (m : M), dist (⇑(v m).weights) q ≤ r) (w : StdSimplex ℝ M) : dist (⇑((affineMapMk v) w).weights) q ≤ r

Every point of an affine simplex lies in each closed ball, for the sup metric on weight vectors, that contains all of its vertices.