Extreme subsets and convex combinations

An injective linear map preserves and reflects extreme points when it identifies the source set with a face of the target set. The scalar assumptions allow semirings and additive monoids, so the result applies to measures with scalars in ℝ≥0∞.

Over a linearly ordered field, an extreme subset B of A absorbs every convex combination with strictly positive weights that it meets, as long as the convex hull of the points combined lies in A: all those points then lie in B (IsExtreme.mem_of_centerMass_mem). Consequently a point of B in the convex hull of s is already in the convex hull of s ∩ B (IsExtreme.convexHull_inter_subset). This is how a triangulation of a convex set restricts to each of its faces.

Every subfamily of an affinely independent family spans an extreme subset of its convex hull (AffineIndependent.isExtreme_convexHull). Thus the faces of a simplex are extreme, without any topological or finite-dimensional assumption.

theorem TauCeti.mem_extremePoints_iff_linearMap_mem_extremePoints {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] {C : Set E} {D D' : Set F} (x : E) (hface : IsExtreme 𝕜 D D') (f : E →ₗ[𝕜] F) (hf : Function.Injective ⇑f) (hmem : ∀ (x : E), f x ∈ D ↔ x ∈ C) (hmaps : Set.MapsTo (⇑f) C D') (hsurj : D' ⊆ Set.range ⇑f) : x ∈ Set.extremePoints 𝕜 C ↔ f x ∈ Set.extremePoints 𝕜 D

A point x is extreme if and only if its image under an injective linear map is extreme, when membership in the target pulls back to the source set, the source maps into a face, and that face lies in the map's range.

theorem IsExtreme.mem_of_centerMass_mem {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {A B : Set E} (hAB : IsExtreme 𝕜 A B) {t : Finset ι} {w : ι → 𝕜} {z : ι → E} (hw : ∀ i ∈ t, 0 < w i) (hzA : (convexHull 𝕜) (z '' ↑t) ⊆ A) (hB : t.centerMass w z ∈ B) {i : ι} (hi : i ∈ t) : z i ∈ B

If a convex combination with strictly positive weights lies in an extreme subset B of a set A which contains the convex hull of the points combined, then each of these points lies in B.

theorem IsExtreme.convexHull_inter_subset {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {A B : Set E} (hAB : IsExtreme 𝕜 A B) {s : Set E} (hsA : (convexHull 𝕜) s ⊆ A) : (convexHull 𝕜) s ∩ B ⊆ (convexHull 𝕜) (s ∩ B)

A point of an extreme subset B of A which is a convex combination of points of s is a convex combination of the points of s lying in B, provided the convex hull of s lies in A.

theorem AffineIndependent.isExtreme_convexHull {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {p : ι → E} (hp : AffineIndependent 𝕜 p) (s : Set ι) : IsExtreme 𝕜 ((convexHull 𝕜) (Set.range p)) ((convexHull 𝕜) (p '' s))

The convex hull of any subfamily of an affinely independent family is an extreme subset of the convex hull of the whole family. In particular, every face of a simplex is extreme.