# 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

## TODO #

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

def IsExtreme (𝕜 : Type u_1) {E : Type u_2} [] [] [SMul 𝕜 E] (A : Set E) (B : Set E) :

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
Instances For
def Set.extremePoints (𝕜 : Type u_1) {E : Type u_2} [] [] [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
Instances For
theorem IsExtreme.refl (𝕜 : Type u_1) {E : Type u_2} [] [] [SMul 𝕜 E] (A : Set E) :
IsExtreme 𝕜 A A
theorem IsExtreme.rfl {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] {A : Set E} :
IsExtreme 𝕜 A A
theorem IsExtreme.trans {𝕜 : Type u_1} {E : Type u_2} [] [] [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} [] [] [SMul 𝕜 E] :
instance instIsPartialOrderSetIsExtreme {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] :
Equations
• =
theorem IsExtreme.inter {𝕜 : Type u_1} {E : Type u_2} [] [] [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} [] [] [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} [] [] [SMul 𝕜 E] {A : Set E} {ι : Sort u_6} [] {F : ιSet E} (hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)) :
IsExtreme 𝕜 A (⋂ (i : ι), F i)
theorem isExtreme_biInter {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] {A : Set E} {F : Set (Set E)} (hF : F.Nonempty) (hA : BF, IsExtreme 𝕜 A B) :
IsExtreme 𝕜 A (BF, B)
theorem isExtreme_sInter {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] {A : Set E} {F : Set (Set E)} (hF : F.Nonempty) (hAF : BF, IsExtreme 𝕜 A B) :
IsExtreme 𝕜 A (⋂₀ F)
theorem mem_extremePoints {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] {A : Set E} {x : E} :
x 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} [] [] [SMul 𝕜 E] {A : Set E} {x : E} :
IsExtreme 𝕜 A {x} x

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} [] [] [SMul 𝕜 E] {A : Set E} {x : E} :
IsExtreme 𝕜 A {x}x

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} [] [] [SMul 𝕜 E] {A : Set E} :
A
@[simp]
theorem extremePoints_empty {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] :
@[simp]
theorem extremePoints_singleton {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] {x : E} :
= {x}
theorem inter_extremePoints_subset_extremePoints_of_subset {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] {A : Set E} {B : Set E} (hBA : B A) :
B
theorem IsExtreme.extremePoints_subset_extremePoints {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] {A : Set E} {B : Set E} (hAB : IsExtreme 𝕜 A B) :
theorem IsExtreme.extremePoints_eq {𝕜 : Type u_1} {E : Type u_2} [] [] [SMul 𝕜 E] {A : Set E} {B : Set E} (hAB : IsExtreme 𝕜 A B) :
= B
theorem IsExtreme.convex_diff {𝕜 : Type u_1} {E : Type u_2} [] [] [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} [] [] [] [Module 𝕜 E] [Module 𝕜 F] (s : Set E) (t : Set F) :
@[simp]
theorem extremePoints_pi {𝕜 : Type u_1} {ι : Type u_4} {π : ιType u_5} [] [(i : ι) → AddCommGroup (π i)] [(i : ι) → Module 𝕜 (π i)] (s : (i : ι) → Set (π 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} [] [] [Module 𝕜 E] [] [Module 𝕜 F] [EquivLike L E F] [LinearEquivClass L 𝕜 E F] (f : L) (s : Set E) :
f '' = Set.extremePoints 𝕜 (f '' s)
theorem mem_extremePoints_iff_forall_segment {𝕜 : Type u_1} {E : Type u_2} [] [Module 𝕜 E] [] [] {A : Set E} {x : E} :
x 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} [] [Module 𝕜 E] [] [] {A : Set E} {x : E} (hA : Convex 𝕜 A) :
x x A Convex 𝕜 (A \ {x})
theorem Convex.mem_extremePoints_iff_mem_diff_convexHull_diff {𝕜 : Type u_1} {E : Type u_2} [] [Module 𝕜 E] [] [] {A : Set E} {x : E} (hA : Convex 𝕜 A) :
x x A \ () (A \ {x})
theorem extremePoints_convexHull_subset {𝕜 : Type u_1} {E : Type u_2} [] [Module 𝕜 E] [] [] {A : Set E} :
Set.extremePoints 𝕜 (() A) A