Documentation

Mathlib.Analysis.Convex.Exposed

Exposed sets #

This file defines exposed sets and exposed points for sets in a real vector space.

An exposed subset of A is a subset of A that is the set of all maximal points of a functional (a continuous linear map E β†’ π•œ) over A. By convention, βˆ… is an exposed subset of all sets. This allows for better functoriality of the definition (the intersection of two exposed subsets is exposed, faces of a polytope form a bounded lattice). This is an analytic notion of "being on the side of". It is stronger than being extreme (see IsExposed.isExtreme), but weaker (for exposed points) than being a vertex.

An exposed set of A is sometimes called a "face of A", but we decided to reserve this terminology to the more specific notion of a face of a polytope (sometimes hopefully soon out on mathlib!).

Main declarations #

References #

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

TODO #

Define intrinsic frontier/interior and prove the lemmas related to exposed sets and points.

Generalise to Locally Convex Topological Vector Spacesβ„’

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

def IsExposed (π•œ : Type u_1) {E : Type u_2} [TopologicalSpace π•œ] [Semiring π•œ] [Preorder π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] (A : Set E) (B : Set E) :

A set B is exposed with respect to A iff it maximizes some functional over A (and contains all points maximizing it). Written IsExposed π•œ A B.

Equations
Instances For
    def ContinuousLinearMap.toExposed {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] (l : E β†’L[π•œ] π•œ) (A : Set E) :
    Set E

    A useful way to build exposed sets from intersecting A with halfspaces (modelled by an inequality with a functional).

    Equations
    Instances For
      theorem ContinuousLinearMap.toExposed.isExposed {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {l : E β†’L[π•œ] π•œ} {A : Set E} :
      theorem isExposed_empty {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} :
      IsExposed π•œ A βˆ…
      theorem IsExposed.subset {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {B : Set E} (hAB : IsExposed π•œ A B) :
      B βŠ† A
      theorem IsExposed.refl {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] (A : Set E) :
      IsExposed π•œ A A
      theorem IsExposed.antisymm {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {B : Set E} (hB : IsExposed π•œ A B) (hA : IsExposed π•œ B A) :
      A = B
      theorem IsExposed.mono {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {B : Set E} {C : Set E} (hC : IsExposed π•œ A C) (hBA : B βŠ† A) (hCB : C βŠ† B) :
      IsExposed π•œ B C
      theorem IsExposed.eq_inter_halfspace' {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {B : Set E} (hAB : IsExposed π•œ A B) (hB : Set.Nonempty B) :
      βˆƒ (l : E β†’L[π•œ] π•œ) (a : π•œ), B = {x : E | x ∈ A ∧ a ≀ l x}

      If B is a nonempty exposed subset of A, then B is the intersection of A with some closed halfspace. The converse is not true. It would require that the corresponding open halfspace doesn't intersect A.

      theorem IsExposed.eq_inter_halfspace {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] [Nontrivial π•œ] {A : Set E} {B : Set E} (hAB : IsExposed π•œ A B) :
      βˆƒ (l : E β†’L[π•œ] π•œ) (a : π•œ), B = {x : E | x ∈ A ∧ a ≀ l x}

      For nontrivial π•œ, if B is an exposed subset of A, then B is the intersection of A with some closed halfspace. The converse is not true. It would require that the corresponding open halfspace doesn't intersect A.

      theorem IsExposed.inter {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] [ContinuousAdd π•œ] {A : Set E} {B : Set E} {C : Set E} (hB : IsExposed π•œ A B) (hC : IsExposed π•œ A C) :
      IsExposed π•œ A (B ∩ C)
      theorem IsExposed.sInter {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} [ContinuousAdd π•œ] {F : Finset (Set E)} (hF : F.Nonempty) (hAF : βˆ€ B ∈ F, IsExposed π•œ A B) :
      IsExposed π•œ A (β‹‚β‚€ ↑F)
      theorem IsExposed.inter_left {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {B : Set E} {C : Set E} (hC : IsExposed π•œ A C) (hCB : C βŠ† B) :
      IsExposed π•œ (A ∩ B) C
      theorem IsExposed.inter_right {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {B : Set E} {C : Set E} (hC : IsExposed π•œ B C) (hCA : C βŠ† A) :
      IsExposed π•œ (A ∩ B) C
      theorem IsExposed.isClosed {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] [OrderClosedTopology π•œ] {A : Set E} {B : Set E} (hAB : IsExposed π•œ A B) (hA : IsClosed A) :
      theorem IsExposed.isCompact {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] [OrderClosedTopology π•œ] [T2Space E] {A : Set E} {B : Set E} (hAB : IsExposed π•œ A B) (hA : IsCompact A) :
      def Set.exposedPoints (π•œ : Type u_1) {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] (A : Set E) :
      Set E

      A point is exposed with respect to A iff there exists a hyperplane whose intersection with A is exactly that point.

      Equations
      Instances For
        theorem exposed_point_def {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {x : E} :
        x ∈ Set.exposedPoints π•œ A ↔ x ∈ A ∧ βˆƒ (l : E β†’L[π•œ] π•œ), βˆ€ y ∈ A, l y ≀ l x ∧ (l x ≀ l y β†’ y = x)
        theorem exposedPoints_subset {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} :
        @[simp]
        theorem exposedPoints_empty {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] :
        theorem mem_exposedPoints_iff_exposed_singleton {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [OrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {x : E} :
        x ∈ Set.exposedPoints π•œ A ↔ IsExposed π•œ A {x}

        Exposed points exactly correspond to exposed singletons.

        theorem IsExposed.convex {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [LinearOrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {B : Set E} (hAB : IsExposed π•œ A B) (hA : Convex π•œ A) :
        Convex π•œ B
        theorem IsExposed.isExtreme {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [LinearOrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} {B : Set E} (hAB : IsExposed π•œ A B) :
        IsExtreme π•œ A B
        theorem exposedPoints_subset_extremePoints {π•œ : Type u_1} {E : Type u_2} [TopologicalSpace π•œ] [LinearOrderedRing π•œ] [AddCommMonoid E] [TopologicalSpace E] [Module π•œ E] {A : Set E} :