mathlib3 documentation

analysis.convex.exposed

Exposed sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 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.

source
def is_exposed (𝕜 : Type u_1) {E : Type u_2} [topological_space 𝕜] [semiring 𝕜] [preorder 𝕜] [add_comm_monoid E] [topological_space 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 is_exposed 𝕜 A B.

Equations
source
def continuous_linear_map.to_exposed {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space 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
source
theorem continuous_linear_map.to_exposed.is_exposed {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {l : E →L[𝕜] 𝕜} {A : set E} :
is_exposed 𝕜 A (l.to_exposed A)
source
theorem is_exposed_empty {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A : set E} :
is_exposed 𝕜 A ∅
source
@[protected]
theorem is_exposed.subset {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A B : set E} (hAB : is_exposed 𝕜 A B) :
B ⊆ A
source
@[protected, refl]
theorem is_exposed.refl {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] (A : set E) :
is_exposed 𝕜 A A
source
@[protected]
theorem is_exposed.antisymm {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A B : set E} (hB : is_exposed 𝕜 A B) (hA : is_exposed 𝕜 B A) :
A = B
source
@[protected]
theorem is_exposed.mono {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A B C : set E} (hC : is_exposed 𝕜 A C) (hBA : B ⊆ A) (hCB : C ⊆ B) :
is_exposed 𝕜 B C
source
theorem is_exposed.eq_inter_halfspace' {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A B : set E} (hAB : is_exposed 𝕜 A B) (hB : B.nonempty) :
∃ (l : E →L[𝕜] 𝕜) (a : 𝕜), B = {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.

source
theorem is_exposed.eq_inter_halfspace {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] [nontrivial 𝕜] {A B : set E} (hAB : is_exposed 𝕜 A B) :
∃ (l : E →L[𝕜] 𝕜) (a : 𝕜), B = {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.

source
@[protected]
theorem is_exposed.inter {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] [has_continuous_add 𝕜] {A B C : set E} (hB : is_exposed 𝕜 A B) (hC : is_exposed 𝕜 A C) :
is_exposed 𝕜 A (B ∩ C)
source
theorem is_exposed.sInter {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A : set E} [has_continuous_add 𝕜] {F : finset (set E)} (hF : F.nonempty) (hAF : ∀ (B : set E), B ∈ F → is_exposed 𝕜 A B) :
is_exposed 𝕜 A (⋂₀ ↑F)
source
theorem is_exposed.inter_left {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A B C : set E} (hC : is_exposed 𝕜 A C) (hCB : C ⊆ B) :
is_exposed 𝕜 (A ∩ B) C
source
theorem is_exposed.inter_right {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A B C : set E} (hC : is_exposed 𝕜 B C) (hCA : C ⊆ A) :
is_exposed 𝕜 (A ∩ B) C
source
@[protected]
theorem is_exposed.is_closed {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] [order_closed_topology 𝕜] {A B : set E} (hAB : is_exposed 𝕜 A B) (hA : is_closed A) :
is_closed B
source
@[protected]
theorem is_exposed.is_compact {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] [order_closed_topology 𝕜] [t2_space E] {A B : set E} (hAB : is_exposed 𝕜 A B) (hA : is_compact A) :
is_compact B
source
def set.exposed_points (𝕜 : Type u_1) {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 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
source
theorem exposed_point_def {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 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)
source
theorem exposed_points_subset {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A : set E} :
set.exposed_points 𝕜 A ⊆ A
source
@[simp]
theorem exposed_points_empty {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] :
set.exposed_points 𝕜 ∅ = ∅
source
theorem mem_exposed_points_iff_exposed_singleton {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A : set E} {x : E} :
x ∈ set.exposed_points 𝕜 A ↔ is_exposed 𝕜 A {x}

Exposed points exactly correspond to exposed singletons.

source
@[protected]
theorem is_exposed.convex {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [linear_ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A B : set E} (hAB : is_exposed 𝕜 A B) (hA : convex 𝕜 A) :
convex 𝕜 B
source
@[protected]
theorem is_exposed.is_extreme {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [linear_ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A B : set E} (hAB : is_exposed 𝕜 A B) :
is_extreme 𝕜 A B
source
theorem exposed_points_subset_extreme_points {𝕜 : Type u_1} {E : Type u_2} [topological_space 𝕜] [linear_ordered_ring 𝕜] [add_comm_monoid E] [topological_space E] [module 𝕜 E] {A : set E} :
set.exposed_points 𝕜 A ⊆ set.extreme_points 𝕜 A