The standard simplex as a join with its barycentre or a vertex

The standard simplex, the set of weight vectors of Convexity.StdSimplex ℝ ι, is the convex join of its relative boundary, the points with some vanishing coordinate, and its barycentre, the constant point (card ι)⁻¹. Along the segment from a boundary point to the barycentre, the position is recovered as card ι times the least coordinate. So the segments meet only at the barycentre, and every point of the simplex other than the barycentre lies on exactly one of them.

This is pseudo-radial projection of a simplex from its barycentre onto its boundary. It identifies the cone on the boundary of a simplex, with apex at the barycentre, with the whole simplex; this is the local model of a closed vertex star whose link is a combinatorial sphere.

Similarly, the standard simplex is the convex join of the facet opposite a vertex i with that vertex, the i-th coordinate recovering the position along each segment. This is the local model of a closed vertex star whose link is a combinatorial ball.

Main results

• Convexity.StdSimplex.mem_range_toFun_comp_weights_iff: the weight vectors of the standard simplex are the vectors with nonnegative coordinates summing to one.
• Convexity.StdSimplex.convex_range_toFun_comp_weights: the weight vectors of the standard simplex form a convex set.
• TauCeti.stdSimplexBoundary, TauCeti.isCompact_stdSimplexBoundary: the relative boundary of the standard simplex, the points with some vanishing coordinate, and its compactness.
• TauCeti.card_mul_inf'_smul_add_smul_barycenter: card ι times the least coordinate recovers the parameter along a segment from a boundary point to the barycentre.
• TauCeti.convexJoin_boundary_stdSimplex_barycenter: the standard simplex is the convex join of its relative boundary with its barycentre.
• TauCeti.convexJoin_facet_stdSimplex_single: the standard simplex is the convex join of a facet with the opposite vertex.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 2, “Pseudo-Radial Projection”, pp. 20–21.

theorem Convexity.StdSimplex.mem_range_toFun_comp_weights_iff {R : Type u_1} [Semiring R] [PartialOrder R] {X : Type u_2} [Fintype X] {x : X → R} : (x ∈ Set.range fun (t : StdSimplex R X) => ⇑t.weights) ↔ (∀ (i : X), 0 ≤ x i) ∧ ∑ i : X, x i = 1

A vector is a weight vector of the standard simplex if and only if its coordinates are nonnegative and sum to one.

theorem Convexity.StdSimplex.convex_range_toFun_comp_weights (R : Type u_1) [Semiring R] [PartialOrder R] [IsOrderedRing R] (X : Type u_2) : Convex R (Set.range fun (t : StdSimplex R X) => ⇑t.weights)

The weight vectors of the standard simplex form a convex set.

theorem Convexity.StdSimplex.apply_lt_one_of_mem_range_weights {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {ι : Type u_2} [Finite ι] {x : ι → R} (hx : x ∈ Set.range fun (s : StdSimplex R ι) => ⇑s.weights) {i j : ι} (hij : j ≠ i) (hxj : 0 < x j) : x i < 1

A coordinate of a point of the standard simplex is less than one if some other coordinate is positive.

def TauCeti.stdSimplexBoundary (ι : Type u_1) : Set (ι → ℝ)

The relative boundary of the standard simplex: its points with some vanishing coordinate.

theorem TauCeti.stdSimplexBoundary_def (ι : Type u_1) : stdSimplexBoundary ι = {y : ι → ℝ | (y ∈ Set.range fun (s : Convexity.StdSimplex ℝ ι) => ⇑s.weights) ∧ ∃ (i : ι), y i = 0}

The relative boundary of the standard simplex is the set of its points with some vanishing coordinate.

@[simp]

theorem TauCeti.mem_stdSimplexBoundary {ι : Type u_1} {x : ι → ℝ} : x ∈ stdSimplexBoundary ι ↔ (x ∈ Set.range fun (s : Convexity.StdSimplex ℝ ι) => ⇑s.weights) ∧ ∃ (i : ι), x i = 0

Membership in the relative boundary of the standard simplex.

theorem TauCeti.stdSimplexBoundary_subset {ι : Type u_1} : stdSimplexBoundary ι ⊆ Set.range fun (s : Convexity.StdSimplex ℝ ι) => ⇑s.weights

The relative boundary lies in the standard simplex.

theorem TauCeti.isCompact_stdSimplexBoundary {ι : Type u_1} [Finite ι] : IsCompact (stdSimplexBoundary ι)

The relative boundary of the standard simplex is compact.

theorem TauCeti.mem_stdSimplexBoundary_or_forall_pos {ι : Type u_1} [Finite ι] {x : ι → ℝ} (hx : x ∈ Set.range fun (s : Convexity.StdSimplex ℝ ι) => ⇑s.weights) : x ∈ stdSimplexBoundary ι ∨ ∀ (i : ι), 0 < x i

A point of the standard simplex lies on its relative boundary or in its open part.

theorem TauCeti.card_mul_inf'_smul_add_smul_barycenter {ι : Type u_1} [Fintype ι] [Nonempty ι] {y : ι → ℝ} (hy : 0 ≤ y) {i : ι} (hi : y i = 0) {t : ℝ} (ht : t ≤ 1) : ↑(Fintype.card ι) * Finset.univ.inf' ⋯ ((1 - t) • y + t • ⇑Convexity.StdSimplex.barycenter.weights) = t

Along the segment from a point y with nonnegative coordinates, one of them zero, to the barycentre of the standard simplex, card ι times the least coordinate is the parameter t.

theorem TauCeti.convexJoin_boundary_stdSimplex_barycenter {ι : Type u_1} [Fintype ι] [Nontrivial ι] : convexJoin ℝ (stdSimplexBoundary ι) {⇑Convexity.StdSimplex.barycenter.weights} = Set.range fun (s : Convexity.StdSimplex ℝ ι) => ⇑s.weights

Pseudo-radial decomposition of the standard simplex. The standard simplex is the convex join of its relative boundary, the points with some vanishing coordinate, with its barycentre.

theorem TauCeti.convexJoin_facet_stdSimplex_single {ι : Type u_1} {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Finite ι] [Nontrivial ι] [DecidableEq ι] (i : ι) : convexJoin R {y : ι → R | (y ∈ Set.range fun (s : Convexity.StdSimplex R ι) => ⇑s.weights) ∧ y i = 0} {Pi.single i 1} = Set.range fun (s : Convexity.StdSimplex R ι) => ⇑s.weights

The standard simplex as a cone on a facet. The standard simplex is the convex join of the facet opposite a vertex i, the points with vanishing i-th coordinate, with that vertex. Along the segment from a point of the facet to the vertex, the i-th coordinate is the parameter.