mathlib documentation

analysis.convex.exposed

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 on mathlib!).

Main declarations #

References #

See chapter 8 of Barry Simon, Convexity

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 is_exposed (π•œ : Type u_1) {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ 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 is_exposed π•œ A B.

Equations
def continuous_linear_map.to_exposed {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ 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
theorem continuous_linear_map.to_exposed.is_exposed {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {l : E β†’L[π•œ] π•œ} {A : set E} :
is_exposed π•œ A (l.to_exposed A)
theorem is_exposed_empty {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A : set E} :
is_exposed π•œ A βˆ…
theorem is_exposed.subset {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A B : set E} (hAB : is_exposed π•œ A B) :
B βŠ† A
theorem is_exposed.refl {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] (A : set E) :
is_exposed π•œ A A
theorem is_exposed.antisymm {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A B : set E} (hB : is_exposed π•œ A B) (hA : is_exposed π•œ B A) :
A = B
theorem is_exposed.mono {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A B C : set E} (hC : is_exposed π•œ A C) (hBA : B βŠ† A) (hCB : C βŠ† B) :
is_exposed π•œ B C
theorem is_exposed.eq_inter_halfspace {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A B : set E} (hAB : is_exposed π•œ A B) :
βˆƒ (l : E β†’L[π•œ] π•œ) (a : π•œ), B = {x ∈ A | a ≀ ⇑l x}

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 is_exposed.inter {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A B C : set E} (hB : is_exposed π•œ A B) (hC : is_exposed π•œ A C) :
is_exposed π•œ A (B ∩ C)
theorem is_exposed.sInter {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A : set E} {F : finset (set E)} (hF : F.nonempty) (hAF : βˆ€ (B : set E), B ∈ F β†’ is_exposed π•œ A B) :
theorem is_exposed.inter_left {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A B C : set E} (hC : is_exposed π•œ A C) (hCB : C βŠ† B) :
is_exposed π•œ (A ∩ B) C
theorem is_exposed.inter_right {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A B C : set E} (hC : is_exposed π•œ B C) (hCA : C βŠ† A) :
is_exposed π•œ (A ∩ B) C
theorem is_exposed.is_extreme {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A B : set E} (hAB : is_exposed π•œ A B) :
is_extreme π•œ A B
theorem is_exposed.convex {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A B : set E} (hAB : is_exposed π•œ A B) (hA : convex π•œ A) :
convex π•œ B
theorem is_exposed.is_closed {E : Type u_2} [normed_group E] {A B : set E} [normed_space ℝ E] (hAB : is_exposed ℝ A B) (hA : is_closed A) :
theorem is_exposed.is_compact {E : Type u_2} [normed_group E] {A B : set E} [normed_space ℝ E] (hAB : is_exposed ℝ A B) (hA : is_compact A) :
def set.exposed_points (π•œ : Type u_1) {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] (A : set E) :
set E

A point is exposed with respect to A iff there exists an hyperplane whose intersection with A is exactly that point.

Equations
theorem exposed_point_def {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A : set E} {x : E} :
x ∈ set.exposed_points π•œ A ↔ x ∈ A ∧ βˆƒ (l : E β†’L[π•œ] π•œ), βˆ€ (y : E), y ∈ A β†’ ⇑l y ≀ ⇑l x ∧ (⇑l x ≀ ⇑l y β†’ y = x)
theorem exposed_points_subset {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A : set E} :
@[simp]
theorem exposed_points_empty {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] :
theorem mem_exposed_points_iff_exposed_singleton {π•œ : Type u_1} {E : Type u_2} [normed_linear_ordered_field π•œ] [normed_group E] [normed_space π•œ E] {A : set E} {x : E} :
x ∈ set.exposed_points π•œ A ↔ is_exposed π•œ A {x}

Exposed points exactly correspond to exposed singletons.