Exposed directions and the exposed representation of a closed convex set

An exposed face of a convex set C is the set on which some continuous linear functional attains its maximum over C; an exposed point is a one-point exposed face, and an exposed direction is the direction of an exposed face that is a closed half-line. Every exposed face is a face, so exposed points are extreme points and exposed directions are extreme directions, but not conversely.

The theorem proved here is that a closed convex set containing no lines is recovered from its exposed points and exposed directions alone, up to closure: C = cl (conv (exp C ∪ expdir C)). Representation.lean gives the same recovery from the extreme points and directions with no closure at all; the closure is the price of passing to the smaller, exposed, data, and it cannot be dropped, because the exposed points of a closed convex set need not be closed. The dual representation — a closed convex set with nonempty interior is the intersection of the closed half-spaces tangent to it — is in Tangent.lean.

Main definitions

• IsExposedDirection C y — the direction of y is an exposed direction of C: some closed half-line in the direction of y is an exposed face of C. exposedDirections C is the set of vectors generating such directions, the analogue for exposedPoints of IsExtremeDirection.

Main results

• exists_forall_sub_le_mul_sub — the multiplier for one linear equation: if g ≤ γ on the slice C ∩ {f = β}, and f takes values on both sides of β on C, then g - γ ≤ c * (f - β) on all of C for some c.
• closure_convexHullPD_exposedPoints_exposedDirections — the exposed representation of a line-free closed convex set.
• closure_coneHull_exposedDirections, closure_coneHull_of_forall_exposedDirection — the cone case: a line-free closed convex cone is the closure of the cone its exposed directions generate.
• isExposed_recessionCone — the recession cone of an exposed face is an exposed face of the recession cone, given that it is contained in it; the exposed analogue of isFace_recessionCone. exposedDirections_subset_exposedDirections_recessionCone is the consequence for closed C, and isExposedDirection_recessionCone its topology-free form.

Implementation notes

The classical proof extends a codimension-two affine set to a supporting hyperplane, which is really a multiplier: exists_forall_sub_le_mul_sub produces it by a one-dimensional argument valid in every dimension. The final case split is then bounded/unbounded rather than by the shape of a one-dimensional face — the bounded case is Minkowski's theorem in every dimension, and only the unbounded case uses dim C' ≤ 1.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §18.

Exposed directions

def Tdaf.ConvexAnalysis.IsExposedDirection {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (C : Set E) (y : E) : Prop

y generates an exposed direction of C: y ≠ 0 and some closed half-line in the direction of y is an exposed face of C. Rockafellar's exposed direction — an "exposed point at infinity" — is the direction itself; representing it by a generating vector avoids a quotient, at the cost of exposedDirections C being closed under multiplication by positive scalars.

Equations

• Tdaf.ConvexAnalysis.IsExposedDirection C y = (y ≠ 0 ∧ ∃ (x : E), IsExposed ℝ C (Tdaf.ConvexAnalysis.halfLine x y))

def Tdaf.ConvexAnalysis.exposedDirections {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (C : Set E) : Set E

The set of vectors that generate exposed directions of C.

Equations

• Tdaf.ConvexAnalysis.exposedDirections C = {y : E | Tdaf.ConvexAnalysis.IsExposedDirection C y}

theorem Tdaf.ConvexAnalysis.mem_exposedDirections {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {C : Set E} {y : E} : y ∈ exposedDirections C ↔ IsExposedDirection C y

Membership in exposedDirections, unfolded.

theorem Tdaf.ConvexAnalysis.IsExposedDirection.isExtremeDirection {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {C : Set E} {y : E} (h : IsExposedDirection C y) : IsExtremeDirection C y

An exposed direction is an extreme direction. The half-line that the exposed face happens to be is a face of C, since it is convex and exposed sets are extreme.

theorem Tdaf.ConvexAnalysis.exposedDirections_subset_extremeDirections {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (C : Set E) : exposedDirections C ⊆ extremeDirections C

Exposed directions are extreme directions.

theorem Tdaf.ConvexAnalysis.IsExposedDirection.smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {C : Set E} {y : E} (h : IsExposedDirection C y) {a : ℝ} (ha : 0 < a) : IsExposedDirection C (a • y)

Exposed directions do not change under positive rescaling of the generator.

theorem Tdaf.ConvexAnalysis.IsExposedDirection.halfLine_subset {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {C : Set E} {y : E} (h : IsExposedDirection C y) : ∃ (x : E), halfLine x y ⊆ C

The half-line in an exposed direction lies in C.

theorem Tdaf.ConvexAnalysis.isExposed_recessionCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {C C' : Set E} (h : IsExposed ℝ C C') (hrec : recessionCone C' ⊆ recessionCone C) : IsExposed ℝ (recessionCone C) (recessionCone C')

The recession cone of an exposed face is an exposed face of the recession cone, exposed by the same functional. The hypothesis 0⁺C' ⊆ 0⁺C supplies the monotonicity the recession cone does not have; the mechanism is that a functional maximised over C is non-positive on 0⁺C and vanishes exactly on the directions in which the face itself recedes.

theorem Tdaf.ConvexAnalysis.isExposedDirection_recessionCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {C : Set E} {y : E} (h : IsExposedDirection C y) (hy : y ∈ recessionCone C) : IsExposedDirection (recessionCone C) y

An exposed direction in which C recedes is an exposed direction of 0⁺C: the exposed analogue of isExtremeDirection_recessionCone, and proved the same way.

Exposed directions of the recession cone

theorem Tdaf.ConvexAnalysis.exposedDirections_subset_exposedDirections_recessionCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {C : Set E} (hC : Convex ℝ C) (hCcl : IsClosed C) : exposedDirections C ⊆ exposedDirections (recessionCone C)

Every exposed direction of a closed convex set is an exposed direction of its recession cone. Closedness enters only in knowing that the direction of a half-line exposed face recedes in C.

A multiplier for one linear equation

theorem Tdaf.ConvexAnalysis.exists_forall_sub_le_mul_sub {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hC : Convex ℝ C) (f g : E →ₗ[ℝ] ℝ) {β γ : ℝ} (hslice : ∀ z ∈ C, f z = β → g z ≤ γ) (hlo : ∃ z ∈ C, f z < β) (hhi : ∃ z ∈ C, β < f z) : ∃ (c : ℝ), ∀ z ∈ C, g z - γ ≤ c * (f z - β)

A linear function dominated on a slice is dominated up to a multiple of the slicing function. If g ≤ γ wherever f = β on a convex set C, and f takes values strictly below and strictly above β on C, then g - γ ≤ c * (f - β) on all of C for some scalar c. Geometrically, the image of C under z ↦ (f z - β, g z - γ) misses the open upward vertical ray, so it lies below a line through the origin, and c is that line's slope. This replaces the "extend an (n-2)-dimensional affine set to a supporting hyperplane" step of the classical proof, and needs no dimension hypothesis.

The exposed representation of a line-free closed convex set

theorem Tdaf.ConvexAnalysis.closure_convexHullPD_exposedPoints_exposedDirections {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Convex ℝ C) (hCcl : IsClosed C) (hnl : ContainsNoLine C) : closure (convexHullPD (Set.exposedPoints ℝ C) (exposedDirections C)) = C

A closed convex set containing no lines is the closure of the convex hull of its exposed points and exposed directions. Unlike the extreme-point representation the closure cannot be dropped — the exposed points of a closed convex set need not be closed, and Straszewicz's theorem only places the extreme points in their closure.

Sketch: if the exposed hull C₀ were not all of C, separate a point of C \ C₀ from C₀ by H = {f = β}. The slice C ∩ H is a nonempty closed convex set containing no lines, so it has an exposed point x, and exists_forall_sub_le_mul_sub turns its exposing functional into one maximised over C at x. Its exposed face C' meets H only at x, which forces x ∈ ri C' and dim C' ≤ 1; a bounded C' is then the hull of its extreme points, an unbounded one a half-line whose direction is exposed, and either way x ∈ C₀.

The cone case

theorem Tdaf.ConvexAnalysis.closure_coneHull_exposedDirections {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Convex ℝ C) (hCcl : IsClosed C) (hne : C.Nonempty) (hcone : ∀ x ∈ C, ∀ (a : ℝ), 0 ≤ a → a • x ∈ C) (hnl : ContainsNoLine C) : closure ↑(PointedCone.hull ℝ (exposedDirections C)) = C

A closed convex cone containing no lines is the closure of the cone generated by its exposed directions. The usual statement assumes the cone contains more than the origin; that is unnecessary, since the zero cone has no exposed directions and PointedCone.hull ℝ ∅ = {0}.

theorem Tdaf.ConvexAnalysis.closure_coneHull_of_forall_exposedDirection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C T : Set E} (hC : Convex ℝ C) (hCcl : IsClosed C) (hne : C.Nonempty) (hcone : ∀ x ∈ C, ∀ (a : ℝ), 0 ≤ a → a • x ∈ C) (hnl : ContainsNoLine C) (hTC : T ⊆ C) (hgen : ∀ y ∈ exposedDirections C, ∃ x ∈ T, ∃ (a : ℝ), 0 < a ∧ y = a • x) : closure ↑(PointedCone.hull ℝ T) = C

The generating form: any set of vectors of a line-free closed convex cone that generates all of its exposed rays generates the cone, up to closure.