# 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 #

• IsExposed π A B: States that B is an exposed set of A (in the literature, A is often implicit).
• IsExposed.isExtreme: An exposed set is also extreme.

## 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 π] [] [] [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 π] [] [] [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 π] [] [] [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 π] [] [] [Module π E] {A : Set E} :
IsExposed π A β
theorem IsExposed.subset {π : Type u_1} {E : Type u_2} [TopologicalSpace π] [OrderedRing π] [] [] [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 π] [] [] [Module π E] (A : Set E) :
IsExposed π A A
theorem IsExposed.antisymm {π : Type u_1} {E : Type u_2} [TopologicalSpace π] [OrderedRing π] [] [] [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 π] [] [] [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 π] [] [] [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 π] [] [] [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 π] [] [] [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 π] [] [] [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 π] [] [] [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 π] [] [] [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 π] [] [] [Module π E] [] {A : Set E} {B : Set E} (hAB : IsExposed π A B) (hA : ) :
theorem IsExposed.isCompact {π : Type u_1} {E : Type u_2} [TopologicalSpace π] [OrderedRing π] [] [] [Module π E] [] [] {A : Set E} {B : Set E} (hAB : IsExposed π A B) (hA : ) :
def Set.exposedPoints (π : Type u_1) {E : Type u_2} [TopologicalSpace π] [OrderedRing π] [] [] [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 π] [] [] [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 π] [] [] [Module π E] {A : Set E} :
@[simp]
theorem exposedPoints_empty {π : Type u_1} {E : Type u_2} [TopologicalSpace π] [OrderedRing π] [] [] [Module π E] :
theorem mem_exposedPoints_iff_exposed_singleton {π : Type u_1} {E : Type u_2} [TopologicalSpace π] [OrderedRing π] [] [] [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 π] [] [] [] [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 π] [] [] [] [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 π] [] [] [] [Module π E] {A : Set E} :