The standard simplex

In this file, given an ordered semiring 𝕜 and a finite type ι, we define stdSimplex : Set (ι → 𝕜) as the set of vectors with non-negative coordinates with total sum 1.

When f : X → Y is a map between finite types, we define the map stdSimplex.map f : stdSimplex 𝕜 X → stdSimplex 𝕜 Y.

def stdSimplex (𝕜 : Type u_2) (ι : Type u_1) [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] : Set (ι → 𝕜)

The standard simplex in the space of functions ι → 𝕜 is the set of vectors with non-negative coordinates with total sum 1. This is the free object in the category of convex spaces.

Equations

• stdSimplex 𝕜 ι = {f : ι → 𝕜 | (∀ (x : ι), 0 ≤ f x) ∧ ∑ x : ι, f x = 1}

theorem stdSimplex_eq_inter (𝕜 : Type u_2) (ι : Type u_1) [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] : stdSimplex 𝕜 ι = (⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | ∑ x : ι, f x = 1}

theorem convex_stdSimplex (𝕜 : Type u_2) (ι : Type u_1) [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] [IsOrderedRing 𝕜] : Convex 𝕜 (stdSimplex 𝕜 ι)

theorem stdSimplex_of_subsingleton (𝕜 : Type u_2) (ι : Type u_1) [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] [Subsingleton 𝕜] : stdSimplex 𝕜 ι = Set.univ

theorem stdSimplex_of_isEmpty_index (𝕜 : Type u_2) (ι : Type u_1) [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] [IsEmpty ι] [Nontrivial 𝕜] : stdSimplex 𝕜 ι = ∅

The standard simplex in the zero-dimensional space is empty.

theorem stdSimplex_unique (𝕜 : Type u_2) (ι : Type u_1) [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] [ZeroLEOneClass 𝕜] [Nonempty ι] [Subsingleton ι] : stdSimplex 𝕜 ι = {fun (x : ι) => 1}

theorem mem_Icc_of_mem_stdSimplex {𝕜 : Type u_2} {ι : Type u_1} [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] [IsOrderedAddMonoid 𝕜] {f : ι → 𝕜} (hf : f ∈ stdSimplex 𝕜 ι) (x : ι) : f x ∈ Set.Icc 0 1

All values of a function f ∈ stdSimplex 𝕜 ι belong to [0, 1].

theorem single_mem_stdSimplex (𝕜 : Type u_2) {ι : Type u_1} [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] [DecidableEq ι] [ZeroLEOneClass 𝕜] (i : ι) : Pi.single i 1 ∈ stdSimplex 𝕜 ι

theorem ite_eq_mem_stdSimplex (𝕜 : Type u_2) {ι : Type u_1} [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] [DecidableEq ι] [ZeroLEOneClass 𝕜] (i : ι) : (fun (x : ι) => if i = x then 1 else 0) ∈ stdSimplex 𝕜 ι

theorem segment_single_subset_stdSimplex (𝕜 : Type u_2) {ι : Type u_1} [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] [DecidableEq ι] [ZeroLEOneClass 𝕜] [IsOrderedRing 𝕜] (i j : ι) : segment 𝕜 (Pi.single i 1) (Pi.single j 1) ⊆ stdSimplex 𝕜 ι

The edges are contained in the simplex.

theorem stdSimplex_fin_two (𝕜 : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [ZeroLEOneClass 𝕜] [IsOrderedRing 𝕜] : stdSimplex 𝕜 (Fin 2) = segment 𝕜 (Pi.single 0 1) (Pi.single 1 1)

def stdSimplexEquivIcc (𝕜 : Type u_1) [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] : ↑(stdSimplex 𝕜 (Fin 2)) ≃ ↑(Set.Icc 0 1)

The standard one-dimensional simplex in Fin 2 → 𝕜 is equivalent to the unit interval. This bijection sends the zeroth vertex Pi.single 0 1 to 0 and the first vertex Pi.single 1 1 to 1.

Equations

• stdSimplexEquivIcc 𝕜 = { toFun := fun (f : ↑(stdSimplex 𝕜 (Fin 2))) => ⟨↑f 1, ⋯⟩, invFun := fun (x : ↑(Set.Icc 0 1)) => ⟨![1 - ↑x, ↑x], ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem stdSimplexEquivIcc_symm_apply_coe (𝕜 : Type u_1) [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] (x : ↑(Set.Icc 0 1)) : ↑((stdSimplexEquivIcc 𝕜).symm x) = ![1 - ↑x, ↑x]

@[simp]

theorem stdSimplexEquivIcc_apply_coe (𝕜 : Type u_1) [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] (f : ↑(stdSimplex 𝕜 (Fin 2))) : ↑((stdSimplexEquivIcc 𝕜) f) = ↑f 1

@[simp]

theorem stdSimplexEquivIcc_zero (𝕜 : Type u_1) [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] : (stdSimplexEquivIcc 𝕜) ⟨Pi.single 0 1, ⋯⟩ = 0

@[simp]

theorem stdSimplexEquivIcc_one (𝕜 : Type u_1) [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] : (stdSimplexEquivIcc 𝕜) ⟨Pi.single 1 1, ⋯⟩ = 1

theorem convexHull_basis_eq_stdSimplex (R : Type u_1) (ι : Type u_2) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Fintype ι] [DecidableEq ι] : (convexHull R) (Set.range fun (i j : ι) => if i = j then 1 else 0) = stdSimplex R ι

stdSimplex 𝕜 ι is the convex hull of the canonical basis in ι → 𝕜.

theorem convexHull_rangle_single_eq_stdSimplex (R : Type u_1) (ι : Type u_2) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Fintype ι] [DecidableEq ι] : (convexHull R) (Set.range fun (i : ι) => Pi.single i 1) = stdSimplex R ι

stdSimplex 𝕜 ι is the convex hull of the points Pi.single i 1 for i : i`.

theorem Set.Finite.convexHull_eq_image {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {E : Type u_3} [AddCommGroup E] [Module R E] {s : Set E} (hs : s.Finite) : (convexHull R) s = ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s

The convex hull of a finite set is the image of the standard simplex in s → ℝ under the linear map sending each function w to ∑ x ∈ s, w x • x.

Since we have no sums over finite sets, we use sum over @Finset.univ _ hs.fintype. The map is defined in terms of operations on (s → ℝ) →ₗ[ℝ] ℝ so that later we will not need to prove that this map is linear.

theorem stdSimplex_subset_closedBall {ι : Type u_1} [Fintype ι] : stdSimplex ℝ ι ⊆ Metric.closedBall 0 1

Every vector in stdSimplex 𝕜 ι has max-norm at most 1.

theorem bounded_stdSimplex (ι : Type u_1) [Fintype ι] : Bornology.IsBounded (stdSimplex ℝ ι)

stdSimplex ℝ ι is bounded.

theorem isClosed_stdSimplex (ι : Type u_1) [Fintype ι] : IsClosed (stdSimplex ℝ ι)

stdSimplex ℝ ι is closed.

theorem isCompact_stdSimplex (ι : Type u_1) [Fintype ι] : IsCompact (stdSimplex ℝ ι)

stdSimplex ℝ ι is compact.

instance stdSimplex.instCompactSpace_coe (ι : Type u_1) [Fintype ι] : CompactSpace ↑(stdSimplex ℝ ι)

def stdSimplexHomeomorphUnitInterval : ↑(stdSimplex ℝ (Fin 2)) ≃ₜ ↑unitInterval

The standard one-dimensional simplex in ℝ² = Fin 2 → ℝ is homeomorphic to the unit interval.

Equations

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

@[simp]

theorem stdSimplexHomeomorphUnitInterval_apply_coe (f : ↑(stdSimplex ℝ (Fin 2))) : ↑(stdSimplexHomeomorphUnitInterval f) = ↑f 1

@[simp]

theorem stdSimplexHomeomorphUnitInterval_symm_apply_coe (x : ↑(Set.Icc 0 1)) : ↑(stdSimplexHomeomorphUnitInterval.symm x) = ![1 - ↑x, ↑x]

@[simp]

theorem stdSimplexHomeomorphUnitInterval_zero : stdSimplexHomeomorphUnitInterval ⟨Pi.single 0 1, ⋯⟩ = 0

@[simp]

theorem stdSimplexHomeomorphUnitInterval_one : stdSimplexHomeomorphUnitInterval ⟨Pi.single 1 1, ⋯⟩ = 1

instance stdSimplex.instFunLikeElemForall {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] : FunLike (↑(stdSimplex S X)) X S

Equations

• stdSimplex.instFunLikeElemForall = { coe := fun (s : ↑(stdSimplex S X)) => ↑s, coe_injective' := ⋯ }

theorem stdSimplex.ext {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] {s t : ↑(stdSimplex S X)} (h : ⇑s = ⇑t) : s = t

theorem stdSimplex.ext_iff {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] {s t : ↑(stdSimplex S X)} : s = t ↔ ⇑s = ⇑t

@[simp]

theorem stdSimplex.zero_le {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] (s : ↑(stdSimplex S X)) (x : X) : 0 ≤ s x

@[simp]

theorem stdSimplex.sum_eq_one {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] (s : ↑(stdSimplex S X)) : ∑ x : X, s x = 1

@[simp]

theorem stdSimplex.le_one {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] (s : ↑(stdSimplex S X)) (x : X) : s x ≤ 1

theorem stdSimplex.image_linearMap {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] (f : X → Y) : ⇑(FunOnFinite.linearMap S S f) '' stdSimplex S X ⊆ stdSimplex S Y

noncomputable def stdSimplex.map {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] (f : X → Y) (s : ↑(stdSimplex S X)) : ↑(stdSimplex S Y)

The map stdSimplex S X → stdSimplex S Y that is induced by a map f : X → Y.

Equations

• stdSimplex.map f s = ⟨(FunOnFinite.linearMap S S f) ⇑s, ⋯⟩

@[simp]

theorem stdSimplex.map_coe {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] (f : X → Y) (s : ↑(stdSimplex S X)) : ⇑(map f s) = (FunOnFinite.linearMap S S f) ⇑s

@[simp]

theorem stdSimplex.map_id_apply {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] (x : ↑(stdSimplex S X)) : map id x = x

theorem stdSimplex.map_comp_apply {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Fintype X] [Fintype Y] [Fintype Z] [IsOrderedRing S] (f : X → Y) (g : Y → Z) (x : ↑(stdSimplex S X)) : map g (map f x) = map (g ∘ f) x

@[reducible, inline]

abbrev stdSimplex.vertex {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [DecidableEq X] (x : X) : ↑(stdSimplex S X)

The vertex corresponding to x : X in stdSimplex S X.

Equations

• stdSimplex.vertex x = ⟨Pi.single x 1, ⋯⟩

@[simp]

theorem stdSimplex.vertex_coe {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [DecidableEq X] (x : X) : ⇑(vertex x) = Pi.single x 1

@[simp]

theorem stdSimplex.map_vertex {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] [DecidableEq X] [DecidableEq Y] (f : X → Y) (x : X) : map f (vertex x) = vertex (f x)

theorem stdSimplex.continuous_map {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] [TopologicalSpace S] [IsTopologicalSemiring S] (f : X → Y) : Continuous (map f)