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

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 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 = (B.Nonempty → ∃ (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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [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 half-spaces (modelled by an inequality with a functional).

Equations

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

theorem ContinuousLinearMap.toExposed.isExposed {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A : Set E} : IsExposed 𝕜 A ∅

theorem IsExposed.subset {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A B : Set E} (hAB : IsExposed 𝕜 A B) : B ⊆ A

theorem IsExposed.refl {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (A : Set E) : IsExposed 𝕜 A A

theorem IsExposed.antisymm {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A 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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A B 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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A 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 half-space. The converse is not true. It would require that the corresponding open half-space doesn't intersect A.

@[deprecated IsExposed.eq_inter_halfSpace' (since := "2024-11-12")]

theorem IsExposed.eq_inter_halfspace' {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A B : Set E} (hAB : IsExposed 𝕜 A B) (hB : B.Nonempty) : ∃ (l : E →L[𝕜] 𝕜) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ l x}

Alias of IsExposed.eq_inter_halfSpace'.

---

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

theorem IsExposed.eq_inter_halfSpace {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] [IsOrderedRing 𝕜] [Nontrivial 𝕜] {A 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 half-space. The converse is not true. It would require that the corresponding open half-space doesn't intersect A.

@[deprecated IsExposed.eq_inter_halfSpace (since := "2024-11-12")]

theorem IsExposed.eq_inter_halfspace {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] [IsOrderedRing 𝕜] [Nontrivial 𝕜] {A B : Set E} (hAB : IsExposed 𝕜 A B) : ∃ (l : E →L[𝕜] 𝕜) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ l x}

Alias of IsExposed.eq_inter_halfSpace.

---

For nontrivial 𝕜, if B is an exposed subset of A, then B is the intersection of A with some closed half-space. The converse is not true. It would require that the corresponding open half-space doesn't intersect A.

theorem IsExposed.inter {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] [IsOrderedRing 𝕜] [ContinuousAdd 𝕜] {A B 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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A : Set E} [IsOrderedRing 𝕜] [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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A B 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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A B 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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] [OrderClosedTopology 𝕜] {A B : Set E} (hAB : IsExposed 𝕜 A B) (hA : IsClosed A) : IsClosed B

theorem IsExposed.isCompact {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] [OrderClosedTopology 𝕜] [T2Space E] {A B : Set E} (hAB : IsExposed 𝕜 A B) (hA : IsCompact A) : IsCompact B

def Set.exposedPoints (𝕜 : Type u_1) {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [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 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : Set.exposedPoints 𝕜 ∅ = ∅

theorem mem_exposedPoints_iff_exposed_singleton {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [PartialOrder 𝕜] [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 𝕜] [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A B : Set E} (hAB : IsExposed 𝕜 A B) (hA : Convex 𝕜 A) : Convex 𝕜 B

theorem IsExposed.isExtreme {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A B : Set E} (hAB : IsExposed 𝕜 A B) : IsExtreme 𝕜 A B

theorem exposedPoints_subset_extremePoints {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace 𝕜] [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] {A : Set E} : Set.exposedPoints 𝕜 A ⊆ Set.extremePoints 𝕜 A