Coordinates on the standard simplex and its affine hull

This file develops algebraic and ordered coordinate constructions for Convexity.StdSimplex R ι. The affine coordinate chart is available over a commutative ring, while statements involving simplex inequalities use a compatible partial order. The final section gives the topological properties of these coordinate charts over ℝ.

For a finite index type ι and a chosen coordinate i : ι, the affine hyperplane ∑ j, u j = 1 is parametrized by the remaining card ι - 1 coordinates, with the omitted coordinate reconstructed as 1 - ∑ j, u j.

The ambient coordinate declarations remain in the root namespace. Declarations whose target is Mathlib's intrinsic simplex are placed in Convexity.StdSimplex. None of this material belongs to a measure-theory namespace.

Main definitions and results

• stdSimplexAffineSet: the affine hyperplane ∑ j, u j = 1.
• stdSimplexAffineBasis: the standard vertices as an affine basis of that hyperplane.
• stdSimplexCoordEquiv: its parametrization by card ι - 1 free coordinates.
• stdSimplexFreeCoords: the filled simplex in free coordinates.
• Convexity.StdSimplex.equivFreeCoords: the corresponding parametrization of Mathlib's intrinsic standard simplex.

The affine hyperplane is identified with Mathlib's fintypeAffineCoords. The standard vertices form an affine basis of this hyperplane, and its barycentric coordinates are the ordinary ambient coordinates. We nevertheless retain the explicit omitted-coordinate chart: its computational formulas are used by the measure and integral theory.

@[reducible, inline]

abbrev stdSimplexAffineSet {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] : Set (ι → R)

The affine hyperplane {x | ∑ j, x j = 1} (the affine hull of the standard simplex), viewed as a plain set. This is the carrier of Mathlib's fintypeAffineCoords.

Equations

• stdSimplexAffineSet = ↑(fintypeAffineCoords ι R)

theorem sum_eq_apply_add_sum_ne {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (u : ι → R) (i : ι) : ∑ j : ι, u j = u i + ∑ j : { j : ι // j ≠ i }, u ↑j

Compatibility name for Fintype.sum_eq_add_sum_subtype_ne.

@[reducible, inline]

abbrev stdSimplexAffineSubspace {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] : AffineSubspace R (ι → R)

The affine hyperplane {x | ∑ j, x j = 1} as an AffineSubspace.

Equations

• stdSimplexAffineSubspace = fintypeAffineCoords ι R

theorem mem_stdSimplexAffineSubspace_iff {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (x : ι → R) : x ∈ stdSimplexAffineSubspace ↔ x ∈ stdSimplexAffineSet

The elements of the affine subspace are exactly the elements of the affine set.

noncomputable def stdSimplexAffineVertex {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) : ↥(fintypeAffineCoords ι R)

The standard vertex indexed by i, regarded as a point of the affine coordinate hyperplane.

Equations

• stdSimplexAffineVertex i = ⟨Pi.single i 1, ⋯⟩

@[simp]

theorem stdSimplexAffineVertex_apply {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i j : ι) : ↑(stdSimplexAffineVertex i) j = if i = j then 1 else 0

The ambient coordinate of a standard affine vertex is a Kronecker delta.

theorem instNonemptySubtypeForallMemAffineSubspaceFintypeAffineCoords_leanPool {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [Nonempty ι] : Nonempty ↥(fintypeAffineCoords ι R)

@[simp]

theorem stdSimplexAffineVertex_subtype_apply {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [Nonempty ι] (i j : ι) : (fintypeAffineCoords ι R).subtype (stdSimplexAffineVertex i) j = if i = j then 1 else 0

Applying the inclusion of the affine coordinate hyperplane to a standard vertex gives the corresponding Kronecker-delta function.

theorem affineIndependent_stdSimplexAffineVertex {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [Nonempty ι] : AffineIndependent R stdSimplexAffineVertex

The standard vertices are affinely independent in the affine coordinate hyperplane.

theorem affineCombination_stdSimplexAffineVertex {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [Nonempty ι] (u : ↥(fintypeAffineCoords ι R)) : (Finset.affineCombination R Finset.univ stdSimplexAffineVertex) ↑u = u

Every point of the affine coordinate hyperplane is the affine combination of the standard vertices with weights given by its ambient coordinates.

theorem affineSpan_stdSimplexAffineVertex {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [Nonempty ι] : affineSpan R (Set.range stdSimplexAffineVertex) = ⊤

The standard vertices affinely span the affine coordinate hyperplane.

noncomputable def stdSimplexAffineBasis {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [Nonempty ι] : AffineBasis ι R ↥(fintypeAffineCoords ι R)

The standard vertices form an affine basis of Mathlib's affine coordinate hyperplane.

Equations

• stdSimplexAffineBasis = { toFun := stdSimplexAffineVertex, ind' := ⋯, tot' := ⋯ }

@[simp]

theorem stdSimplexAffineBasis_apply {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [Nonempty ι] (i : ι) : stdSimplexAffineBasis i = stdSimplexAffineVertex i

The points of stdSimplexAffineBasis are the standard affine vertices.

@[simp]

theorem stdSimplexAffineBasis_coord {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [Nonempty ι] (i : ι) (u : ↥(fintypeAffineCoords ι R)) : (stdSimplexAffineBasis.coord i) u = ↑u i

Barycentric coordinates for the standard affine basis are the ordinary ambient coordinates.

def stdSimplexCoordProj {ι : Type u_1} {R : Type u_2} (i : ι) (u : ι → R) : { j : ι // j ≠ i } → R

The coordinate projection that eliminates coordinate i.

Equations

• stdSimplexCoordProj i u j = u ↑j

noncomputable def stdSimplexCoordMap {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) (x : { j : ι // j ≠ i } → R) : ι → R

Map from the free-coordinate space that omits coordinate i to stdSimplexAffineSet, constructed by pairing the recovered dependent coordinate with x, then applying the inverse of Equiv.funSplitAt i R.

Equations

• stdSimplexCoordMap i x = (Equiv.funSplitAt i R).symm (1 - ∑ j : { j : ι // j ≠ i }, x j, x)

@[simp]

theorem stdSimplexCoordMap_apply_self {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) (x : { j : ι // j ≠ i } → R) : stdSimplexCoordMap i x i = 1 - ∑ j : { j : ι // j ≠ i }, x j

The value of the dependent coordinate i is 1 - ∑ j, x j.

@[simp]

theorem stdSimplexCoordMap_apply_of_ne {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i j : ι) (h : j ≠ i) (x : { j : ι // j ≠ i } → R) : stdSimplexCoordMap i x j = x ⟨j, h⟩

The value of a free coordinate j ≠ i remains unchanged under the coordinate map.

@[simp]

theorem sum_stdSimplexCoordMap {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) (x : { j : ι // j ≠ i } → R) : ∑ j : ι, stdSimplexCoordMap i x j = 1

The coordinate map maps to stdSimplexAffineSet.

@[simp]

theorem stdSimplexCoordProj_coordMap {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) (x : { j : ι // j ≠ i } → R) : stdSimplexCoordProj i (stdSimplexCoordMap i x) = x

Projecting after applying the coordinate map recovers the free coordinates.

theorem stdSimplexCoordMap_coordProj {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) {u : ι → R} (hu : u ∈ stdSimplexAffineSet) : stdSimplexCoordMap i (stdSimplexCoordProj i u) = u

Applying the coordinate map after projecting recovers the vector on stdSimplexAffineSet.

theorem range_stdSimplexCoordMap {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) : Set.range (stdSimplexCoordMap i) = stdSimplexAffineSet

The range of stdSimplexCoordMap is the affine hyperplane stdSimplexAffineSet.

theorem stdSimplexCoordMap_comp_perm {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) (σ : Equiv.Perm ι) (x : { j : ι // j ≠ σ i } → R) : stdSimplexCoordMap (σ i) x ∘ ⇑σ = stdSimplexCoordMap i fun (x_1 : { j : ι // j ≠ i }) => match x_1 with | ⟨j, hj⟩ => x ⟨σ j, ⋯⟩

The coordinate map relates stdSimplexCoordMap (σ i) composed with σ to stdSimplexCoordMap i applied to the permuted free coordinates.

noncomputable def stdSimplexFreeCoordSwapLinear {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i j : ι) (hij : i ≠ j) : ({ q : ι // q ≠ i } → R) →ₗ[R] { q : ι // q ≠ i } → R

The linear part of the change of free coordinates induced by swapping the omitted coordinate i with a different coordinate j.

Equations

• One or more equations did not get rendered due to their size.

theorem sum_stdSimplexFreeCoordSwapLinear {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i j : ι) (hij : i ≠ j) (x : { q : ι // q ≠ i } → R) : ∑ q : { q : ι // q ≠ i }, (stdSimplexFreeCoordSwapLinear i j hij) x q = -x ⟨j, ⋯⟩

The sum of the coordinates after applying stdSimplexFreeCoordSwapLinear is the negative of the coordinate belonging to j.

noncomputable def stdSimplexFreeCoordSwap {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i j : ι) (hij : i ≠ j) (x : { q : ι // q ≠ i } → R) : { q : ι // q ≠ i } → R

The affine change of free coordinates induced by swapping i and j in the ambient coordinate space.

Equations

• stdSimplexFreeCoordSwap i j hij x = (fun (q : { q : ι // q ≠ i }) => if q = ⟨j, ⋯⟩ then 1 else 0) + (stdSimplexFreeCoordSwapLinear i j hij) x

@[simp]

theorem stdSimplexFreeCoordSwap_apply_ji {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i j : ι) (hij : i ≠ j) (x : { q : ι // q ≠ i } → R) : stdSimplexFreeCoordSwap i j hij x ⟨j, ⋯⟩ = 1 - ∑ q : { q : ι // q ≠ i }, x q

At the free coordinate corresponding to j, the coordinate swap stores the dependent coordinate recovered from x.

@[simp]

theorem stdSimplexFreeCoordSwap_apply_of_ne {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i j : ι) (hij : i ≠ j) {x : { q : ι // q ≠ i } → R} {q : { q : ι // q ≠ i }} (hq : q ≠ ⟨j, ⋯⟩) : stdSimplexFreeCoordSwap i j hij x q = x q

A free coordinate other than the one corresponding to j is unchanged by the coordinate swap.

@[simp]

theorem sum_stdSimplexFreeCoordSwap {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i j : ι) (hij : i ≠ j) (x : { q : ι // q ≠ i } → R) : ∑ q : { q : ι // q ≠ i }, stdSimplexFreeCoordSwap i j hij x q = 1 - x ⟨j, ⋯⟩

The sum of the coordinates after applying stdSimplexFreeCoordSwap.

theorem stdSimplexCoordMap_comp_freeCoordSwap {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i j : ι) (hij : i ≠ j) : (fun (u : ι → R) => u ∘ ⇑(Equiv.swap i j)) ∘ stdSimplexCoordMap i = stdSimplexCoordMap i ∘ stdSimplexFreeCoordSwap i j hij

Swapping i and j in ambient coordinates corresponds to stdSimplexFreeCoordSwap in the chart omitting i.

noncomputable def stdSimplexCoordEquiv {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) : ({ j : ι // j ≠ i } → R) ≃ ↑stdSimplexAffineSet

The free coordinates obtained by omitting i are equivalent to stdSimplexAffineSet.

Equations

• One or more equations did not get rendered due to their size.

theorem injective_stdSimplexCoordMap {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] (i : ι) : Function.Injective (stdSimplexCoordMap i)

The coordinate map is injective.

def stdSimplexFreeCoords {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [PartialOrder R] (i : ι) : Set ({ j : ι // j ≠ i } → R)

The filled (card ι - 1)-dimensional simplex of free coordinates corresponding to points of Convexity.StdSimplex.coordinateSet R ι. (Not to be confused with Convexity.StdSimplex.coordinateSet R {j // j ≠ i}.)

Equations

• stdSimplexFreeCoords i = {x : { j : ι // j ≠ i } → R | (∀ (j : { j : ι // j ≠ i }), 0 ≤ x j) ∧ ∑ j : { j : ι // j ≠ i }, x j ≤ 1}

noncomputable def Convexity.StdSimplex.equivFreeCoords {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [PartialOrder R] [IsOrderedRing R] (i : ι) : ↑(stdSimplexFreeCoords i) ≃ StdSimplex R ι

Omitted-coordinate parametrization of Mathlib's intrinsic standard simplex.

The forward map stores the reconstructed coordinates as finitely supported weights; the inverse map drops coordinate i. This is the algebraic precursor of the corresponding homeomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Convexity.StdSimplex.weights_equivFreeCoords_apply {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [PartialOrder R] [IsOrderedRing R] (i : ι) (x : ↑(stdSimplexFreeCoords i)) (j : ι) : ((equivFreeCoords i) x).weights j = stdSimplexCoordMap i (↑x) j

The weights of the intrinsic simplex point associated to free coordinates are the coordinates reconstructed by stdSimplexCoordMap.

@[simp]

theorem Convexity.StdSimplex.coe_equivFreeCoords_symm_apply {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [PartialOrder R] [IsOrderedRing R] (i : ι) (s : StdSimplex R ι) : ↑((equivFreeCoords i).symm s) = stdSimplexCoordProj i fun (j : ι) => s.weights j

The inverse of equivFreeCoords drops the chosen coordinate from the weight function.

theorem isClosed_stdSimplexAffineSet {ι : Type u_1} [Fintype ι] : IsClosed stdSimplexAffineSet

stdSimplexAffineSet is closed over the reals.

theorem continuous_stdSimplexFreeCoordSwap {ι : Type u_1} [Fintype ι] (i j : ι) (hij : i ≠ j) : Continuous (stdSimplexFreeCoordSwap i j hij)

The free-coordinate swap is continuous over the reals.

theorem continuous_stdSimplexCoordMap {ι : Type u_1} [Fintype ι] (i : ι) : Continuous (stdSimplexCoordMap i)

The real coordinate map is continuous.

theorem continuous_stdSimplexCoordProj {ι : Type u_1} (i : ι) : Continuous (stdSimplexCoordProj i)

The real coordinate projection is continuous.

noncomputable def stdSimplexCoordHomeomorph {ι : Type u_1} [Fintype ι] (i : ι) : ({ j : ι // j ≠ i } → ℝ) ≃ₜ ↑stdSimplexAffineSet

The real free-coordinate equivalence with stdSimplexAffineSet is a homeomorphism.

Equations

• stdSimplexCoordHomeomorph i = { toEquiv := stdSimplexCoordEquiv i, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem isClosedEmbedding_stdSimplexCoordMap {ι : Type u_1} [Fintype ι] (i : ι) : Topology.IsClosedEmbedding (stdSimplexCoordMap i)

The real coordinate map gives a closed embedding.