The intrinsic simplex and its finite coordinate realization

Convexity.StdSimplex is the simplex object. Its coordinateSet is the carrier of its realization in the ambient vector space, used for measures, restrictions, and neighborhoods. The membership description is kept explicit for ambient calculus; range_coordinates identifies it with the intrinsic object.

The intrinsic simplex uses Mathlib's topology and compactness instance. For finite index types, Mathlib's coordinate embedding identifies this topology with the topology induced by the weights.

def Convexity.StdSimplex.coordinates {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} (s : StdSimplex R ι) : ι → R

The ambient coordinate function of an intrinsic simplex point.

Equations

• s.coordinates i = s.weights i

def Convexity.StdSimplex.coordinateSet (R : Type u_3) (ι : Type u_4) [Semiring R] [PartialOrder R] [Fintype ι] : Set (ι → R)

The coordinate carrier of the intrinsic simplex, not a second simplex type.

Equations

• Convexity.StdSimplex.coordinateSet R ι = {u : ι → R | (∀ (i : ι), 0 ≤ u i) ∧ ∑ i : ι, u i = 1}

theorem Convexity.StdSimplex.mem_coordinateSet {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] {u : ι → R} : u ∈ coordinateSet R ι ↔ (∀ (i : ι), 0 ≤ u i) ∧ ∑ i : ι, u i = 1

theorem Convexity.StdSimplex.coordinates_mem {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] (s : StdSimplex R ι) : s.coordinates ∈ coordinateSet R ι

noncomputable def Convexity.StdSimplex.ofCoordinates {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] (u : ι → R) (hu : u ∈ coordinateSet R ι) : StdSimplex R ι

Recover an intrinsic point from its ambient coordinates and membership proof.

Equations

• Convexity.StdSimplex.ofCoordinates u hu = { weights := Finsupp.equivFunOnFinite.symm u, nonneg := ⋯, total := ⋯ }

@[simp]

theorem Convexity.StdSimplex.coordinates_ofCoordinates {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] (u : ι → R) (hu : u ∈ coordinateSet R ι) : (ofCoordinates u hu).coordinates = u

@[simp]

theorem Convexity.StdSimplex.ofCoordinates_coordinates {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] (s : StdSimplex R ι) : ofCoordinates s.coordinates ⋯ = s

theorem Convexity.StdSimplex.coordinates_injective {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} : Function.Injective coordinates

theorem Convexity.StdSimplex.range_coordinates {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] : Set.range coordinates = coordinateSet R ι

noncomputable def Convexity.StdSimplex.coordinateEquiv {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] : StdSimplex R ι ≃ ↑(coordinateSet R ι)

The intrinsic simplex is equivalent to its coordinate carrier.

Equations

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

theorem Convexity.StdSimplex.mem_Icc_of_mem_coordinateSet {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] [IsOrderedAddMonoid R] {u : ι → R} (hu : u ∈ coordinateSet R ι) (i : ι) : u i ∈ Set.Icc 0 1

theorem Convexity.StdSimplex.coordinateSet_empty {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] [Nontrivial R] [IsEmpty ι] : coordinateSet R ι = ∅

theorem Convexity.StdSimplex.isClosed_coordinateSet (R : Type u_1) [Semiring R] [PartialOrder R] (ι : Type u_2) [Fintype ι] [TopologicalSpace R] [OrderClosedTopology R] [ContinuousAdd R] : IsClosed (coordinateSet R ι)

theorem Convexity.StdSimplex.isCompact_coordinateSet (R : Type u_1) [Semiring R] [PartialOrder R] (ι : Type u_2) [Fintype ι] [TopologicalSpace R] [OrderClosedTopology R] [ContinuousAdd R] [CompactIccSpace R] [IsOrderedAddMonoid R] : IsCompact (coordinateSet R ι)

instance Convexity.StdSimplex.instCompactSpaceElemForallCoordinateSetOfCompactIccSpaceOfIsOrderedAddMonoid {R : Type u_1} [Semiring R] [PartialOrder R] {ι : Type u_2} [Fintype ι] [TopologicalSpace R] [OrderClosedTopology R] [ContinuousAdd R] [CompactIccSpace R] [IsOrderedAddMonoid R] : CompactSpace ↑(coordinateSet R ι)

theorem Convexity.StdSimplex.isEmbedding_coordinates {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [TopologicalSpace R] [IsTopologicalRing R] {ι : Type u_2} [Finite ι] : Topology.IsEmbedding coordinates

theorem Convexity.StdSimplex.continuous_coordinates {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [TopologicalSpace R] [IsTopologicalRing R] {ι : Type u_2} [Finite ι] : Continuous coordinates

noncomputable def Convexity.StdSimplex.coordinateHomeomorph {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [TopologicalSpace R] [IsTopologicalRing R] {ι : Type u_2} [Fintype ι] : StdSimplex R ι ≃ₜ ↑(coordinateSet R ι)

The intrinsic simplex and its coordinate realization have the same topology.

Equations

• Convexity.StdSimplex.coordinateHomeomorph = { toEquiv := Convexity.StdSimplex.coordinateEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem Convexity.StdSimplex.isClosedEmbedding_coordinates {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [TopologicalSpace R] [IsTopologicalRing R] {ι : Type u_2} [Finite ι] [OrderClosedTopology R] : Topology.IsClosedEmbedding coordinates

@[instance_reducible]

noncomputable instance Convexity.StdSimplex.instMeasurableSpaceRealCarlson {ι : Type u_2} : MeasurableSpace (StdSimplex ℝ ι)

Equations

• Convexity.StdSimplex.instMeasurableSpaceRealCarlson = borel (Convexity.StdSimplex ℝ ι)

instance Convexity.StdSimplex.instBorelSpaceRealCarlson {ι : Type u_2} : BorelSpace (StdSimplex ℝ ι)

theorem Convexity.StdSimplex.measurableEmbedding_coordinates {ι : Type u_2} [Finite ι] : MeasurableEmbedding coordinates