The coordinate simplex as a convex body

The coordinate simplex is the set of nonnegative coordinate vectors with total mass at most one. Unlike the barycentric simplex, it is full dimensional: the missing mass is the coordinate of its vertex at the origin. Its frontier consists of the points with a zero coordinate or total mass one. This identifies the proper barycentric faces with a geometric boundary, and allows Mathlib's convex-body rescaling theorem to identify that boundary with a round sphere. Affine vertex swaps transport the neighbourhood of the origin to the neighbourhoods of the other vertices.

Reference: C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2. The sphere identification uses Mathlib's exists_homeomorph_image_interior_closure_frontier_eq_unitBall by Yury Kudryashov.

def TauCeti.coordinateSimplex (ι : Type u_1) [Fintype ι] : Set (ι → ℝ)

The full-dimensional simplex spanned by the origin and the coordinate unit vectors.

@[simp]

theorem TauCeti.mem_coordinateSimplex (ι : Type u_1) [Fintype ι] (x : ι → ℝ) : x ∈ coordinateSimplex ι ↔ (∀ (i : ι), 0 ≤ x i) ∧ ∑ i : ι, x i ≤ 1

Membership in the coordinate simplex is nonnegativity and a bound on total mass.

theorem TauCeti.sum_lt_one_or_exists_pos {ι : Type u_1} [Fintype ι] (x : ι → ℝ) : ∑ i : ι, x i < 1 ∨ ∃ (j : ι), 0 < x j

Every point has positive missing mass 1 - ∑ i, x i or a positive coordinate: its barycentric coordinates, including the missing mass, sum to one.

noncomputable def TauCeti.coordinateSimplexVertexSwap {ι : Type u_1} [Fintype ι] (j : ι) : (ι → ℝ) →ᴬ[ℝ] ι → ℝ

The affine involution exchanging the origin vertex with the jth coordinate vertex of the coordinate simplex. It replaces coordinate j by the missing barycentric mass.

theorem TauCeti.coordinateSimplexVertexSwap_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) (x : ι → ℝ) (i : ι) : (coordinateSimplexVertexSwap j) x i = if i = j then 1 - ∑ k : ι, x k else x i

The swapped coordinate is the missing mass; all other coordinates are unchanged.

@[simp]

theorem TauCeti.sum_coordinateSimplexVertexSwap {ι : Type u_1} [Fintype ι] (j : ι) (x : ι → ℝ) : ∑ i : ι, (coordinateSimplexVertexSwap j) x i = 1 - x j

The total mass after a vertex swap is one minus the original swapped coordinate.

@[simp]

theorem TauCeti.coordinateSimplexVertexSwap_coordinateSimplexVertexSwap {ι : Type u_1} [Fintype ι] (j : ι) (x : ι → ℝ) : (coordinateSimplexVertexSwap j) ((coordinateSimplexVertexSwap j) x) = x

Swapping a vertex with the origin twice is the identity on the ambient space.

@[simp]

theorem TauCeti.coordinateSimplexVertexSwap_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) : (coordinateSimplexVertexSwap j) 0 = Pi.single j 1

The vertex swap sends the origin to the chosen coordinate vertex.

@[simp]

theorem TauCeti.coordinateSimplexVertexSwap_single {ι : Type u_1} [Fintype ι] [DecidableEq ι] (j : ι) : (coordinateSimplexVertexSwap j) (Pi.single j 1) = 0

The vertex swap sends the chosen coordinate vertex to the origin.

theorem TauCeti.coordinateSimplexVertexSwap_mem_iff {ι : Type u_1} [Fintype ι] (j : ι) (x : ι → ℝ) : (coordinateSimplexVertexSwap j) x ∈ coordinateSimplex ι ↔ x ∈ coordinateSimplex ι

Vertex swapping preserves and reflects membership in the full coordinate simplex.

noncomputable def TauCeti.coordinateSimplexVertexSwapHomeomorph {ι : Type u_1} [Fintype ι] (j : ι) : (ι → ℝ) ≃ₜ (ι → ℝ)

The ambient homeomorphism exchanging the origin and a coordinate vertex.

@[simp]

theorem TauCeti.coordinateSimplexVertexSwapHomeomorph_apply {ι : Type u_1} [Fintype ι] (j : ι) (x : ι → ℝ) : (coordinateSimplexVertexSwapHomeomorph j) x = (coordinateSimplexVertexSwap j) x

The vertex homeomorphism applies the affine vertex swap.

@[simp]

theorem TauCeti.coordinateSimplexVertexSwapHomeomorph_symm_apply {ι : Type u_1} [Fintype ι] (j : ι) (x : ι → ℝ) : (coordinateSimplexVertexSwapHomeomorph j).symm x = (coordinateSimplexVertexSwap j) x

The inverse vertex homeomorphism uses the same affine involution.

theorem TauCeti.coordinateSimplexVertexSwap_mem_frontier_iff {ι : Type u_1} [Fintype ι] (j : ι) (x : ι → ℝ) : (coordinateSimplexVertexSwap j) x ∈ frontier (coordinateSimplex ι) ↔ x ∈ frontier (coordinateSimplex ι)

A vertex swap preserves the geometric boundary of the coordinate simplex.

noncomputable def TauCeti.coordinateSimplexChartSwap {ι : Type u_1} [Fintype ι] (v : Option ι) : (ι → ℝ) →ᴬ[ℝ] ι → ℝ

Move a chart's vertex to the origin: none denotes the origin and some j denotes the jth coordinate vertex.

@[simp]

theorem TauCeti.coordinateSimplexChartSwap_none {ι : Type u_1} [Fintype ι] (x : ι → ℝ) : (coordinateSimplexChartSwap none) x = x

The origin chart leaves the ambient coordinates unchanged.

@[simp]

theorem TauCeti.coordinateSimplexChartSwap_some {ι : Type u_1} [Fintype ι] (j : ι) (x : ι → ℝ) : (coordinateSimplexChartSwap (some j)) x = (coordinateSimplexVertexSwap j) x

A coordinate-vertex chart swaps that vertex with the origin.

@[simp]

theorem TauCeti.coordinateSimplexChartSwap_coordinateSimplexChartSwap {ι : Type u_1} [Fintype ι] (v : Option ι) (x : ι → ℝ) : (coordinateSimplexChartSwap v) ((coordinateSimplexChartSwap v) x) = x

The chart vertex swap is an involution.

theorem TauCeti.coordinateSimplexChartSwap_mem_iff {ι : Type u_1} [Fintype ι] (v : Option ι) (x : ι → ℝ) : (coordinateSimplexChartSwap v) x ∈ coordinateSimplex ι ↔ x ∈ coordinateSimplex ι

A chart vertex swap preserves the coordinate simplex.

theorem TauCeti.coordinateSimplexChartSwap_mem_frontier_iff {ι : Type u_1} [Fintype ι] (v : Option ι) (x : ι → ℝ) : (coordinateSimplexChartSwap v) x ∈ frontier (coordinateSimplex ι) ↔ x ∈ frontier (coordinateSimplex ι)

A chart vertex swap preserves the geometric boundary of the coordinate simplex.

theorem TauCeti.convex_coordinateSimplex (ι : Type u_1) [Fintype ι] : Convex ℝ (coordinateSimplex ι)

The coordinate simplex is convex.

theorem TauCeti.isClosed_coordinateSimplex (ι : Type u_1) [Fintype ι] : IsClosed (coordinateSimplex ι)

The coordinate simplex is closed.

theorem TauCeti.coordinateSimplex_subset_Icc (ι : Type u_1) [Fintype ι] : coordinateSimplex ι ⊆ Set.Icc 0 1

Every coordinate of a point of the simplex lies in the unit interval.

theorem TauCeti.isCompact_coordinateSimplex (ι : Type u_1) [Fintype ι] : IsCompact (coordinateSimplex ι)

The coordinate simplex is compact, including in dimension zero.

theorem TauCeti.interior_coordinateSimplex (ι : Type u_1) [Fintype ι] : interior (coordinateSimplex ι) = {x : ι → ℝ | (∀ (i : ι), 0 < x i) ∧ ∑ i : ι, x i < 1}

The interior of the coordinate simplex consists of positive vectors with mass less than one.

theorem TauCeti.isOpen_setOf_sum_lt_one_coordinateSimplex (ι : Type u_1) [Fintype ι] : IsOpen {y : ↑(coordinateSimplex ι) | ∑ i : ι, ↑y i < 1}

The points of the coordinate simplex whose coordinate sum is less than one form an open set in its subtype topology.

@[simp]

theorem TauCeti.mem_frontier_coordinateSimplex (ι : Type u_1) [Fintype ι] (x : ι → ℝ) : x ∈ frontier (coordinateSimplex ι) ↔ ((∀ (i : ι), 0 ≤ x i) ∧ ∑ i : ι, x i ≤ 1) ∧ ((∃ (i : ι), x i = 0) ∨ ∑ i : ι, x i = 1)

A point lies on the frontier exactly when it is in the simplex and at least one of its barycentric coordinates, including the missing mass, vanishes.

theorem TauCeti.nonempty_interior_coordinateSimplex (ι : Type u_1) [Fintype ι] : (interior (coordinateSimplex ι)).Nonempty

The coordinate simplex has nonempty interior.

theorem TauCeti.exists_homeomorph_coordinateSimplex (ι : Type u_1) [Fintype ι] : ∃ (e : (ι → ℝ) ≃ₜ EuclideanSpace ℝ ι), ⇑e '' coordinateSimplex ι = Metric.closedBall 0 1 ∧ ⇑e '' interior (coordinateSimplex ι) = Metric.ball 0 1 ∧ ⇑e '' frontier (coordinateSimplex ι) = Metric.sphere 0 1

An ambient homeomorphism identifies the coordinate simplex, its interior and its frontier with the Euclidean unit closed ball, open ball and sphere, respectively.