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} [OrderedSemiring 𝕜] [AddCommMonoid E] [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} [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
    Instances For
      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] :
      instance instIsPartialOrderSetIsExtreme {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] :
      Equations
      • =
      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 : F.Nonempty) (hA : BF, IsExtreme 𝕜 A B) :
      IsExtreme 𝕜 A (⋂ BF, B)
      theorem isExtreme_sInter {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [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} [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} :
      @[simp]
      theorem extremePoints_empty {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] :
      @[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) :
      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) :
      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) :
      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) :
      @[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.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} [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