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 functioriality 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
is_exposed.is_extreme), 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
Main declarations #
is_exposed 𝕜 A B: States that
Bis an exposed set of
A(in the literature,
Ais often implicit).
is_exposed.is_extreme: An exposed set is also extreme.
See chapter 8 of Barry Simon, Convexity
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
B is exposed with respect to
A iff it maximizes some functional over
A (and contains
all points maximizing it). Written
is_exposed 𝕜 A B.
A useful way to build exposed sets from intersecting
A with halfspaces (modelled by an
inequality with a functional).
B is an exposed subset of
B is the intersection of
A with some closed
halfspace. The converse is not true. It would require that the corresponding open halfspace
A point is exposed with respect to
A iff there exists an hyperplane whose intersection with
A is exactly that point.