Coordinate realization of the standard simplex

This file connects ambient coordinate charts to the intrinsic Convexity.StdSimplex. The coordinate carrier is used for restricting the hyperplane measure and for ambient calculus. The chart homeomorphism targets the intrinsic simplex itself.

@[simp]

theorem preimage_stdSimplex_perm {ι : Type u_1} [Fintype ι] {R : Type u_2} [Semiring R] [PartialOrder R] (σ : Equiv.Perm ι) : (fun (u : ι → R) => u ∘ ⇑σ) ⁻¹' Convexity.StdSimplex.coordinateSet R ι = Convexity.StdSimplex.coordinateSet R ι

The coordinate realization of the standard simplex is invariant under precomposition by a permutation of its coordinates.

@[simp]

theorem preimage_stdSimplexCoordMap {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [PartialOrder R] [IsOrderedRing R] (i : ι) : stdSimplexCoordMap i ⁻¹' Convexity.StdSimplex.coordinateSet R ι = stdSimplexFreeCoords i

The preimage of the coordinate realization of the standard simplex under stdSimplexCoordMap i is stdSimplexFreeCoords i.

@[simp]

theorem stdSimplexCoordMap_mem_stdSimplex_iff {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [PartialOrder R] [IsOrderedRing R] (i : ι) (x : { j : ι // j ≠ i } → R) : stdSimplexCoordMap i x ∈ Convexity.StdSimplex.coordinateSet R ι ↔ x ∈ stdSimplexFreeCoords i

Pointwise form of preimage_stdSimplexCoordMap.

theorem stdSimplexAggregate_mem_stdSimplex {ι : Type u_1} [Fintype ι] {R : Type u_2} [CommRing R] [PartialOrder R] [IsOrderedRing R] {κ : Type u_3} [Fintype κ] {f : ι → κ} {u : ι → R} (hu : u ∈ Convexity.StdSimplex.coordinateSet R ι) : stdSimplexAggregate f u ∈ Convexity.StdSimplex.coordinateSet R κ

Coordinate aggregation sends the coordinate realization of the standard simplex on ι into the coordinate realization on κ.

@[simp]

theorem Convexity.StdSimplex.coordinates_map {ι : Type u_1} [Fintype ι] {R : Type u_2} {κ : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Finite κ] (f : ι → κ) (s : StdSimplex R ι) : (map f s).coordinates = stdSimplexAggregate f s.coordinates

Intrinsic aggregation is realized by summing ambient coordinates over fibers.

noncomputable def Convexity.StdSimplex.homeomorphFreeCoords {ι : Type u_1} [Fintype ι] (i : ι) : ↑(stdSimplexFreeCoords i) ≃ₜ StdSimplex ℝ ι

The omitted-coordinate chart identifies the filled free-coordinate simplex with the intrinsic standard simplex.

Equations

• Convexity.StdSimplex.homeomorphFreeCoords i = { toEquiv := Convexity.StdSimplex.equivFreeCoords i, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Convexity.StdSimplex.coordinates_homeomorphFreeCoords {ι : Type u_1} [Fintype ι] (i : ι) (x : ↑(stdSimplexFreeCoords i)) : ((homeomorphFreeCoords i) x).coordinates = stdSimplexCoordMap i ↑x

@[simp]

theorem Convexity.StdSimplex.coe_homeomorphFreeCoords_symm {ι : Type u_1} [Fintype ι] (i : ι) (s : StdSimplex ℝ ι) : ↑((homeomorphFreeCoords i).symm s) = stdSimplexCoordProj i s.coordinates