Documentation

Mathlib.Analysis.Convex.Extreme

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 #

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.

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

In order to prove that x is an extreme point of A, it is convenient to use mem_extremePoints_iff_left to avoid repeating arguments twice.

Equations
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.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] :
instance instIsPartialOrderSetIsExtreme {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] :
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 : BF, IsExtreme 𝕜 A B) :
IsExtreme 𝕜 A (⋂ BF, 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 : BF, 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
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

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

The definition of extremePoints also requires x₂ = x, but this condition is redundant.

@[simp]
theorem isExtreme_singleton {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {A : Set E} {x : E} :

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} :
@[simp]
theorem extremePoints_empty {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] :
@[simp]
theorem extremePoints_singleton {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} :
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) :
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) :
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) :
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) :
@[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