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.

More not-yet-PRed stuff is available on the mathlib3 branch sperner_again.

def IsExtreme (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (A : Set E) (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.

Equations

• IsExtreme 𝕜 A B = (B ⊆ A ∧ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x : E⦄, x ∈ B → x ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ B ∧ x₂ ∈ B)

def Set.extremePoints (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [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 ∧ x₂ = x}

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

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

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

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

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

Equations

• (_ : IsPartialOrder (Set E) (IsExtreme 𝕜)) = (_ : IsPartialOrder (Set E) (IsExtreme 𝕜))

theorem IsExtreme.inter {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {B : Set E} {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} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {B : Set E} {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} [OrderedSemiring 𝕜] [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} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {F : Set (Set E)} (hF : Set.Nonempty F) (hA : ∀ B ∈ F, IsExtreme 𝕜 A B) : IsExtreme 𝕜 A (⋂ B ∈ F, B)

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

theorem mem_extremePoints {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [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

@[simp]

theorem isExtreme_singleton {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [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} [OrderedSemiring 𝕜] [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} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} : Set.extremePoints 𝕜 A ⊆ A

@[simp]

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

@[simp]

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

theorem inter_extremePoints_subset_extremePoints_of_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {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} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {B : Set E} (hAB : IsExtreme 𝕜 A B) : Set.extremePoints 𝕜 B ⊆ Set.extremePoints 𝕜 A

theorem IsExtreme.extremePoints_eq {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {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} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} {B : Set E} (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} [OrderedSemiring 𝕜] [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} {π : ι → Type u_5} [OrderedSemiring 𝕜] [(i : ι) → AddCommGroup (π i)] [(i : ι) → Module 𝕜 (π i)] (s : (i : ι) → Set (π i)) : Set.extremePoints 𝕜 (Set.pi Set.univ s) = Set.pi Set.univ fun (i : ι) => Set.extremePoints 𝕜 (s i)

theorem image_extremePoints {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {L : Type u_6} [OrderedRing 𝕜] [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} [LinearOrderedRing 𝕜] [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} [LinearOrderedRing 𝕜] [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} [LinearOrderedRing 𝕜] [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} [LinearOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] {A : Set E} : Set.extremePoints 𝕜 ((convexHull 𝕜) A) ⊆ A