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.

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