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

TODO #

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

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
    • l.toExposed A = {x : E | x A yA, l y l x}
    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} :
      IsExposed 𝕜 A (l.toExposed A)
      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

      IsExposed is not transitive: Consider a (topologically) open cube with vertices A₀₀₀, ..., A₁₁₁ and add to it the triangle A₀₀₀A₀₀₁A₀₁₀. Then A₀₀₁A₀₁₀ is an exposed subset of A₀₀₀A₀₀₁A₀₁₀ which is an exposed subset of the cube, but A₀₀₁A₀₁₀ is not itself an exposed subset of the cube.

      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 : B.Nonempty) :
      ∃ (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 : BF, 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[𝕜] 𝕜), yA, l y l x (l x l yy = 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