Extreme sets

This file defines extreme sets and extreme points for sets in a module.

An extreme set of A is a subset of A that is as far as it can get in any outward direction: If point x is in it and point y ∈ A, then the line passing through x and y leaves A at x. This is an analytic notion of "being on the side of". It is weaker than being exposed (see IsExposed.isExtreme).

Main declarations

• IsExtreme 𝕜 A B: States that B is an extreme set of A (in the literature, A is often implicit).
• Set.extremePoints 𝕜 A: Set of extreme points of A (corresponding to extreme singletons).
• Convex.mem_extremePoints_iff_convex_diff: A useful equivalent condition to being an extreme point: x is an extreme point iff A \ {x} is convex.

Implementation notes

The exact definition of extremeness has been carefully chosen so as to make as many lemmas unconditional (in particular, the Krein-Milman theorem doesn't need the set to be convex!). In practice, A is often assumed to be a convex set.

References

See chapter 8 of [Barry Simon, Convexity][simon2011]

TODO

Prove lemmas relating extreme sets and points to the intrinsic frontier.

structure IsExtreme (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (A B : Set E) : Prop

A set B is an extreme subset of A if B ⊆ A and all points of B only belong to open segments whose ends are in B.

Our definition only requires that the left endpoint of the segment lies in B, but by symmetry of open segments, the right endpoint must also lie in B. See IsExtreme.right_mem_of_mem_openSegment.

• subset : B ⊆ A
• left_mem_of_mem_openSegment ⦃x : E⦄ : x ∈ A → ∀ ⦃y : E⦄, y ∈ A → ∀ ⦃z : E⦄, z ∈ B → z ∈ openSegment 𝕜 x y → x ∈ B

theorem isExtreme_iff (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (A B : Set E) : IsExtreme 𝕜 A B ↔ B ⊆ A ∧ ∀ ⦃x : E⦄, x ∈ A → ∀ ⦃y : E⦄, y ∈ A → ∀ ⦃z : E⦄, z ∈ B → z ∈ openSegment 𝕜 x y → x ∈ B

def Set.extremePoints (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (A : Set E) : Set E

A point x is an extreme point of a set A if x belongs to no open segment with ends in A, except for the obvious openSegment x x.

Equations

• Set.extremePoints 𝕜 A = {x : E | x ∈ A ∧ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x}

theorem IsExtreme.refl (𝕜 : Type u_1) {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (A : Set E) : IsExtreme 𝕜 A A

theorem IsExtreme.rfl {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} : IsExtreme 𝕜 A A

theorem IsExtreme.right_mem_of_mem_openSegment {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A B : Set E} {x : E} (h : IsExtreme 𝕜 A B) {y z : E} (hx : x ∈ A) (hy : y ∈ A) (hz : z ∈ B) (hzxy : z ∈ openSegment 𝕜 x y) : y ∈ B

theorem IsExtreme.trans {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A B C : Set E} (hAB : IsExtreme 𝕜 A B) (hBC : IsExtreme 𝕜 B C) : IsExtreme 𝕜 A C

theorem IsExtreme.antisymm {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : AntiSymmetric (IsExtreme 𝕜)

instance instIsPartialOrderSetIsExtreme {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : IsPartialOrder (Set E) (IsExtreme 𝕜)

theorem IsExtreme.inter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A B C : Set E} (hAB : IsExtreme 𝕜 A B) (hAC : IsExtreme 𝕜 A C) : IsExtreme 𝕜 A (B ∩ C)

theorem IsExtreme.mono {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A B C : Set E} (hAC : IsExtreme 𝕜 A C) (hBA : B ⊆ A) (hCB : C ⊆ B) : IsExtreme 𝕜 B C

theorem isExtreme_iInter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {ι : Sort u_6} [Nonempty ι] {F : ι → Set E} (hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)) : IsExtreme 𝕜 A (⋂ (i : ι), F i)

theorem isExtreme_biInter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {F : Set (Set E)} (hF : F.Nonempty) (hA : ∀ B ∈ F, IsExtreme 𝕜 A B) : IsExtreme 𝕜 A (⋂ B ∈ F, B)

theorem isExtreme_sInter {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {F : Set (Set E)} (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExtreme 𝕜 A B) : IsExtreme 𝕜 A (⋂₀ F)

theorem mem_extremePoints {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {x : E} : x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

A point x is an extreme point of a set A iff x ∈ A and for any x₁, x₂ such that x belongs to the open segment (x₁, x₂), we have x₁ = x and x₂ = x.

We used to use the RHS as the definition of extremePoints. However, the conclusion x₂ = x is redundant, so we changed the definition to the RHS of mem_extremePoints_iff_left.

theorem mem_extremePoints_iff_left {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {x : E} : x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x

A point x is an extreme point of a set A iff x ∈ A and for any x₁, x₂ such that x belongs to the open segment (x₁, x₂), we have x₁ = x.

@[simp]

theorem isExtreme_singleton {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {x : E} : IsExtreme 𝕜 A {x} ↔ x ∈ Set.extremePoints 𝕜 A

x is an extreme point to A iff {x} is an extreme set of A.

theorem IsExtreme.mem_extremePoints {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {x : E} : IsExtreme 𝕜 A {x} → x ∈ Set.extremePoints 𝕜 A

Alias of the forward direction of isExtreme_singleton.

---

x is an extreme point to A iff {x} is an extreme set of A.

theorem extremePoints_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} : Set.extremePoints 𝕜 A ⊆ A

@[simp]

theorem extremePoints_empty {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] : Set.extremePoints 𝕜 ∅ = ∅

@[simp]

theorem extremePoints_singleton {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} : Set.extremePoints 𝕜 {x} = {x}

theorem inter_extremePoints_subset_extremePoints_of_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A B : Set E} (hBA : B ⊆ A) : B ∩ Set.extremePoints 𝕜 A ⊆ Set.extremePoints 𝕜 B

theorem IsExtreme.extremePoints_subset_extremePoints {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A B : Set E} (hAB : IsExtreme 𝕜 A B) : Set.extremePoints 𝕜 B ⊆ Set.extremePoints 𝕜 A

theorem IsExtreme.extremePoints_eq {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A B : Set E} (hAB : IsExtreme 𝕜 A B) : Set.extremePoints 𝕜 B = B ∩ Set.extremePoints 𝕜 A

theorem IsExtreme.convex_diff {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {A B : Set E} [IsOrderedRing 𝕜] (hA : Convex 𝕜 A) (hAB : IsExtreme 𝕜 A B) : Convex 𝕜 (A \ B)

@[simp]

theorem extremePoints_prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (s : Set E) (t : Set F) : Set.extremePoints 𝕜 (s ×ˢ t) = Set.extremePoints 𝕜 s ×ˢ Set.extremePoints 𝕜 t

@[simp]

theorem extremePoints_pi {𝕜 : Type u_1} {ι : Type u_4} {M : ι → Type u_5} [Semiring 𝕜] [PartialOrder 𝕜] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module 𝕜 (M i)] (s : (i : ι) → Set (M i)) : Set.extremePoints 𝕜 (Set.univ.pi s) = Set.univ.pi fun (i : ι) => Set.extremePoints 𝕜 (s i)

theorem image_extremePoints {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {L : Type u_6} [Ring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [EquivLike L E F] [LinearEquivClass L 𝕜 E F] (f : L) (s : Set E) : ⇑f '' Set.extremePoints 𝕜 s = Set.extremePoints 𝕜 (⇑f '' s)

theorem mem_extremePoints_iff_forall_segment {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] {A : Set E} {x : E} : x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

A useful restatement using segment: x is an extreme point iff the only (closed) segments that contain it are those with x as one of their endpoints.

theorem Convex.mem_extremePoints_iff_convex_diff {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] {A : Set E} {x : E} (hA : Convex 𝕜 A) : x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ Convex 𝕜 (A \ {x})

theorem Convex.mem_extremePoints_iff_mem_diff_convexHull_diff {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] {A : Set E} {x : E} (hA : Convex 𝕜 A) : x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜) (A \ {x})

theorem extremePoints_convexHull_subset {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] {A : Set E} : Set.extremePoints 𝕜 ((convexHull 𝕜) A) ⊆ A