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 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (A : Set E) (B : Set E) : Prop

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

• IsExposed 𝕜 A B = (Set.Nonempty B → ∃ (l : E →L[𝕜] 𝕜), B = {x : E | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x})

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

• ContinuousLinearMap.toExposed l A = {x : E | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}

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 (ContinuousLinearMap.toExposed l 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 : 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) : IsClosed B

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) : IsCompact B

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

• Set.exposedPoints 𝕜 A = {x : E | x ∈ A ∧ ∃ (l : E →L[𝕜] 𝕜), ∀ y ∈ A, l y ≤ l x ∧ (l x ≤ l y → y = x)}

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} : Set.exposedPoints 𝕜 A ⊆ A

@[simp]

theorem exposedPoints_empty {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [OrderedRing 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : Set.exposedPoints 𝕜 ∅ = ∅

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} : Set.exposedPoints 𝕜 A ⊆ Set.extremePoints 𝕜 A