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 thatB
is an exposed set ofA
(in the literature,A
is often implicit).IsExposed.isExtreme
: An exposed set is also extreme.
References #
See chapter 8 of Barry Simon, Convexity
TODO #
Prove lemmas relating exposed sets and points to the intrinsic frontier.
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
A useful way to build exposed sets from intersecting A
with halfspaces (modelled by an
inequality with a functional).
Instances For
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.
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
.
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
.
A point is exposed with respect to A
iff there exists a hyperplane whose intersection with
A
is exactly that point.
Equations
Instances For
Exposed points exactly correspond to exposed singletons.