Rockafellar, §18: Extreme Points and Faces of Convex Sets

The facial structure of a convex set, the internal representations C = conv S and C = cl (conv S) it produces, and the external representation dual to the second.

All sixteen numbered results of §18 are formalized over Rn n = ℝⁿ: Theorems 18.1–18.8 and Corollaries 18.1.1–18.1.3, 18.3.1, 18.5.1–18.5.3, 18.7.1.

A face is the backbone's IsFace, Rockafellar's definition verbatim, and an extreme point is Mathlib's Set.extremePoints ℝ, a zero-dimensional face. A direction is recorded by a generating vector rather than by a quotient, so extremeDirections C is closed under positive scaling; and conv S, for S a set of points and directions, is convexHullPD P D.

Several statements here are more general than the book's, or supply what it omits. theorem_18_1 and theorem_18_3 drop hypotheses the book states. theorem_18_5_lineality is the "obvious extension" of Theorem 18.5 to a closed convex set of arbitrary lineality, which the book states in words and never proves, and facesEquivFacesInterOrthogonal is the face correspondence it asserts "evidently" on p. 166. Corollaries 18.5.2 and 18.7.1 do not need the cone to contain more than the origin, and Corollary 18.7.1 is printed with no proof at all.

References

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

Faces (p. 162)

theorem Rockafellar.isFace_iff {n : ℕ} {C C' : Set (TdafSurface.Rn n)} : Tdaf.ConvexAnalysis.IsFace C C' ↔ Convex ℝ C' ∧ C' ⊆ C ∧ ∀ x ∈ C, ∀ y ∈ C, ∀ z ∈ C', z ∈ openSegment ℝ x y → x ∈ C' ∧ y ∈ C'

§18 (p. 162). A face of a convex set C is a convex subset C' of C such that every closed line segment in C with a relative interior point in C' has both endpoints in C'. Convexity of C' is a genuine extra requirement: {0, 1} is an extreme subset of [0, 1] but not a face of it.

theorem Rockafellar.isFace_self {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : Tdaf.ConvexAnalysis.IsFace C C

theorem Rockafellar.isFace_empty {n : ℕ} {C : Set (TdafSurface.Rn n)} : Tdaf.ConvexAnalysis.IsFace C ∅

theorem Rockafellar.isFace_trans {n : ℕ} {C C' C₁ : Set (TdafSurface.Rn n)} (h₁ : Tdaf.ConvexAnalysis.IsFace C C') (h₂ : Tdaf.ConvexAnalysis.IsFace C' C₁) : Tdaf.ConvexAnalysis.IsFace C C₁

theorem Rockafellar.isFace_mono {n : ℕ} {C C' D : Set (TdafSurface.Rn n)} (h : Tdaf.ConvexAnalysis.IsFace C C') (hDC : D ⊆ C) (hC'D : C' ⊆ D) : Tdaf.ConvexAnalysis.IsFace D C'

§18 (p. 163). A face of C is a fortiori a face of any convex D with C' ⊆ D ⊆ C.

theorem Rockafellar.isFace_singleton_iff {n : ℕ} {C : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} : Tdaf.ConvexAnalysis.IsFace C {x} ↔ x ∈ Set.extremePoints ℝ C

§18 (p. 162). The extreme points of C are its zero-dimensional faces.

theorem Rockafellar.mem_extremePoints_iff {n : ℕ} {C : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} : x ∈ Set.extremePoints ℝ C ↔ x ∈ C ∧ ∀ y ∈ C, ∀ z ∈ C, ∀ (l : ℝ), 0 < l → l < 1 → x = (1 - l) • y + l • z → y = x ∧ z = x

§18 (p. 162), the book's wording: x ∈ C is extreme iff x = (1 - λ) y + λ z with y, z ∈ C and 0 < λ < 1 forces y = z = x.

The lattice of faces (p. 164)

theorem Rockafellar.faces_isGLB {n : ℕ} {C : Set (TdafSurface.Rn n)} {F : Set (Set (TdafSurface.Rn n))} (hF : F.Nonempty) (h : ∀ B ∈ F, Tdaf.ConvexAnalysis.IsFace C B) : Tdaf.ConvexAnalysis.IsFace C (⋂₀ F) ∧ IsGLB F (⋂₀ F)

§18 (p. 164). A non-empty intersection of faces of C is a face, and is their greatest lower bound in F(C).

theorem Rockafellar.faces_isLUB {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (F : Set (Set (TdafSurface.Rn n))) (h : ∀ B ∈ F, Tdaf.ConvexAnalysis.IsFace C B) : ∃ (G : Set (TdafSurface.Rn n)), Tdaf.ConvexAnalysis.IsFace C G ∧ (∀ B ∈ F, B ⊆ G) ∧ ∀ (G' : Set (TdafSurface.Rn n)), Tdaf.ConvexAnalysis.IsFace C G' → (∀ B ∈ F, B ⊆ G') → G ⊆ G'

§18 (p. 164). Every set of faces of C has a least upper bound in F(C); with faces_isGLB this makes F(C) a complete lattice under inclusion.

Theorem 18.1 and its corollaries

theorem Rockafellar.theorem_18_1 {n : ℕ} {C C' D : Set (TdafSurface.Rn n)} (hface : Tdaf.ConvexAnalysis.IsFace C C') (hDC : D ⊆ C) (h : (intrinsicInterior ℝ D ∩ C').Nonempty) : D ⊆ C'

Theorem 18.1. If C' is a face of C and D ⊆ C has a relative interior point in C', then D ⊆ C'. The book also assumes D convex; the proof uses only the prolongation lemma of §6, which says nothing about D beyond ri D.

theorem Rockafellar.corollary_18_1_1 {n : ℕ} {C C' : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hface : Tdaf.ConvexAnalysis.IsFace C C') : C' = C ∩ closure C'

Corollary 18.1.1. A face of a convex set C satisfies C' = C ∩ cl C'.

theorem Rockafellar.corollary_18_1_1_isClosed {n : ℕ} {C C' : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) (hface : Tdaf.ConvexAnalysis.IsFace C C') : IsClosed C'

Corollary 18.1.1, second sentence: a face of a closed convex set is closed.

theorem Rockafellar.corollary_18_1_2 {n : ℕ} {C C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Tdaf.ConvexAnalysis.IsFace C C₁) (h₂ : Tdaf.ConvexAnalysis.IsFace C C₂) (h : (intrinsicInterior ℝ C₁ ∩ intrinsicInterior ℝ C₂).Nonempty) : C₁ = C₂

Corollary 18.1.2. Two faces of C whose relative interiors meet are equal.

theorem Rockafellar.corollary_18_1_3 {n : ℕ} {C C' : Set (TdafSurface.Rn n)} (hface : Tdaf.ConvexAnalysis.IsFace C C') (hne : C' ≠ C) : C' ⊆ relbd C

Corollary 18.1.3. A face of C other than C lies in the relative boundary of C.

theorem Rockafellar.corollary_18_1_3_dim {n : ℕ} {C C' : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hface : Tdaf.ConvexAnalysis.IsFace C C') (hne' : C'.Nonempty) (hne : C' ≠ C) : dim C' < dim C

Corollary 18.1.3, the dimension statement: a non-empty face other than C itself has dim C' < dim C.

Theorem 18.2: the relative interiors of the faces partition C

theorem Rockafellar.theorem_18_2_union {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) : C = ⋃ C' ∈ {B : Set (TdafSurface.Rn n) | Tdaf.ConvexAnalysis.IsFace C B}, intrinsicInterior ℝ C'

Theorem 18.2, the union half: the relative interiors of the faces of C cover C. (ri ∅ = ∅, so the empty face contributes nothing.)

theorem Rockafellar.theorem_18_2_disjoint {n : ℕ} {C C₁ C₂ : Set (TdafSurface.Rn n)} (h₁ : Tdaf.ConvexAnalysis.IsFace C C₁) (h₂ : Tdaf.ConvexAnalysis.IsFace C C₂) (hne : C₁ ≠ C₂) : Disjoint (intrinsicInterior ℝ C₁) (intrinsicInterior ℝ C₂)

Theorem 18.2, the disjointness half: the relative interiors of distinct faces are disjoint, so with theorem_18_2_union they partition C.

theorem Rockafellar.theorem_18_2_subset {n : ℕ} {C D : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hD : Convex ℝ D) (hDC : D ⊆ C) (hne : D.Nonempty) (hopen : IsRelativelyOpen D) : ∃ (C' : Set (TdafSurface.Rn n)), Tdaf.ConvexAnalysis.IsFace C C' ∧ D ⊆ intrinsicInterior ℝ C'

Theorem 18.2, the containment half: every non-empty relatively open convex subset of C lies in the relative interior of some face.

theorem Rockafellar.theorem_18_2_maximal {n : ℕ} {C C' D : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hface : Tdaf.ConvexAnalysis.IsFace C C') (hne' : C'.Nonempty) (hD : Convex ℝ D) (hopen : IsRelativelyOpen D) (hsub : intrinsicInterior ℝ C' ⊆ D) (hDC : D ⊆ C) : D = intrinsicInterior ℝ C'

Theorem 18.2, the maximality half: the relative interiors of the non-empty faces of C are exactly the maximal relatively open convex subsets of C.

Theorem 18.3: the faces of a hull of points and directions

theorem Rockafellar.theorem_18_3 {n : ℕ} {C' P D : Set (TdafSurface.Rn n)} (hface : Tdaf.ConvexAnalysis.IsFace (Tdaf.ConvexAnalysis.convexHullPD P D) C') : C' = Tdaf.ConvexAnalysis.convexHullPD (P ∩ C') {y : TdafSurface.Rn n | y ∈ D ∧ y ∈ Tdaf.ConvexAnalysis.recessionCone C'}

Theorem 18.3. If C = conv S for a set S of points and directions and C' is a face of C, then C' = conv S', where S' consists of the points of S lying in C' and the directions of S in which C' recedes. The book's hypothesis that C' be non-empty is not needed.

theorem Rockafellar.corollary_18_3_1_points {n : ℕ} (P D : Set (TdafSurface.Rn n)) : Set.extremePoints ℝ (Tdaf.ConvexAnalysis.convexHullPD P D) ⊆ P

Corollary 18.3.1, first half: every extreme point of conv S is a point of S.

theorem Rockafellar.corollary_18_3_1_directions {n : ℕ} (P D : Set (TdafSurface.Rn n)) (hP : ∀ (x z : TdafSurface.Rn n), Bornology.IsBounded (P ∩ Tdaf.ConvexAnalysis.halfLine x z)) {y : TdafSurface.Rn n} (hy : y ∈ Tdaf.ConvexAnalysis.extremeDirections (Tdaf.ConvexAnalysis.convexHullPD P D)) : ∃ z ∈ D, ∃ (a : ℝ), 0 < a ∧ y = a • z

Corollary 18.3.1, second half: if no half-line contains an unbounded set of points of S, every extreme direction of conv S is a direction of S — a positive multiple of a vector of D.

theorem Rockafellar.corollary_18_3_1_directions_of_isBounded {n : ℕ} (P D : Set (TdafSurface.Rn n)) (hP : Bornology.IsBounded P) {y : TdafSurface.Rn n} (hy : y ∈ Tdaf.ConvexAnalysis.extremeDirections (Tdaf.ConvexAnalysis.convexHullPD P D)) : ∃ z ∈ D, ∃ (a : ℝ), 0 < a ∧ y = a • z

Corollary 18.3.1, second half in the case the book highlights: all points of S bounded.

Theorem 18.4: a closed convex set is the hull of its relative boundary

theorem Rockafellar.theorem_18_4 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) (hhalf : ¬Tdaf.ConvexAnalysis.IsAffineHalf C) {x : TdafSurface.Rn n} (hx : x ∈ intrinsicInterior ℝ C) : ∃ a ∈ relbd C, ∃ b ∈ relbd C, x ∈ segment ℝ a b

Theorem 18.4. If a closed convex set C is neither an affine set nor a closed half of one, every relative interior point of C lies on a segment joining two relative boundary points. The book's two exceptional cases are the single predicate IsAffineHalf: allowing the functional to be 0 makes "affine set" the degenerate case of "closed half of an affine set".

Theorem 18.5: the fundamental internal representation

theorem Rockafellar.theorem_18_5 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine C) : Tdaf.ConvexAnalysis.convexHullPD (Set.extremePoints ℝ C) (Tdaf.ConvexAnalysis.extremeDirections C) = C

Theorem 18.5. A closed convex set containing no lines is conv S, for S the set of its extreme points and extreme directions.

theorem Rockafellar.theorem_18_5_lineality {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) : C = ↑(Tdaf.ConvexAnalysis.linealitySubmodule C) + Tdaf.ConvexAnalysis.convexHullPD (Set.extremePoints ℝ (C ∩ ↑(Tdaf.ConvexAnalysis.linealitySubmodule C)ᗮ)) (Tdaf.ConvexAnalysis.extremeDirections (C ∩ ↑(Tdaf.ConvexAnalysis.linealitySubmodule C)ᗮ))

Theorem 18.5 for a closed convex set of arbitrary lineality — the "obvious extension" of p. 166, which the book states in words and never proves. With L the lineality space of C and C₀ = C ∩ L^⊥, one has C = L + conv S₀ for S₀ the extreme points and extreme directions of C₀; C₀ contains no lines because the direction of such a line would lie in both L and L^⊥.

theorem Rockafellar.eq_add_inter_orthogonal_of_isFace {n : ℕ} {C C' : Set (TdafSurface.Rn n)} (h : Tdaf.ConvexAnalysis.IsFace C C') : C' = ↑(Tdaf.ConvexAnalysis.linealitySubmodule C) + C' ∩ ↑(Tdaf.ConvexAnalysis.linealitySubmodule C)ᗮ

§18 (p. 166). A face splits as C' = C₀' + L, with L the lineality space of C and C₀' = C' ∩ L^⊥: a face absorbs the lineality of the set it is a face of.

noncomputable def Rockafellar.facesEquivFacesInterOrthogonal {n : ℕ} (A : Set (TdafSurface.Rn n)) : { C' : Set (TdafSurface.Rn n) // Tdaf.ConvexAnalysis.IsFace A C' } ≃ { C₀ : Set (TdafSurface.Rn n) // Tdaf.ConvexAnalysis.IsFace (A ∩ ↑(Tdaf.ConvexAnalysis.linealitySubmodule A)ᗮ) C₀ }

§18 (p. 166). With L the lineality space of C and C₀ = C ∩ L^⊥, the faces of C correspond one-to-one with those of C₀, by C' = C₀' + L and C₀' = C' ∩ L^⊥. The book asserts this "evidently"; nothing in it needs C closed, convex or finite-dimensional, only that L^⊥ is a complement of L.

Equations

• Rockafellar.facesEquivFacesInterOrthogonal A = Tdaf.ConvexAnalysis.isFaceEquivInter ⋯ ⋯

theorem Rockafellar.corollary_18_5_1 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) (hbdd : Bornology.IsBounded C) : (convexHull ℝ) (Set.extremePoints ℝ C) = C

Corollary 18.5.1 (Minkowski's theorem). A closed bounded convex set is the convex hull of its extreme points.

theorem Rockafellar.corollary_18_5_3 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine C) (hne : C.Nonempty) : (Set.extremePoints ℝ C).Nonempty

Corollary 18.5.3. A non-empty closed convex set containing no lines has an extreme point.

Rays of a convex cone (p. 162)

For a cone the useful zero-dimensional object is not an extreme point — the origin is the only candidate — but an extreme ray: a face which is a half-line emanating from the origin.

def Rockafellar.IsExtremeRay {n : ℕ} (K : Set (TdafSurface.Rn n)) (y : TdafSurface.Rn n) : Prop

§18 (p. 162). An extreme ray of a convex cone K is a face of K which is a half-line emanating from the origin, recorded by a generating vector.

Equations

• Rockafellar.IsExtremeRay K y = (y ≠ 0 ∧ Tdaf.ConvexAnalysis.IsFace K (Tdaf.ConvexAnalysis.halfLine 0 y))

def Rockafellar.IsExposedRay {n : ℕ} (K : Set (TdafSurface.Rn n)) (y : TdafSurface.Rn n) : Prop

§18 (p. 162). An exposed ray of a convex cone K is an exposed face of K which is a half-line emanating from the origin.

Equations

• Rockafellar.IsExposedRay K y = (y ≠ 0 ∧ IsExposed ℝ K (Tdaf.ConvexAnalysis.halfLine 0 y))

theorem Rockafellar.eq_zero_of_isExtreme_halfLine {n : ℕ} {K : Set (TdafSurface.Rn n)} (hne : K.Nonempty) (hcone : ∀ x ∈ K, ∀ (a : ℝ), 0 ≤ a → a • x ∈ K) {x y : TdafSurface.Rn n} (hy : y ≠ 0) (h : IsExtreme ℝ K (Tdaf.ConvexAnalysis.halfLine x y)) : x = 0

A half-line extreme subset of a cone starts at the origin. This is the content of the book's assertion that the extreme rays of a convex cone are in one-to-one correspondence with its extreme directions.

theorem Rockafellar.isExtremeRay_iff_isExtremeDirection {n : ℕ} {K : Set (TdafSurface.Rn n)} (hne : K.Nonempty) (hcone : ∀ x ∈ K, ∀ (a : ℝ), 0 ≤ a → a • x ∈ K) {y : TdafSurface.Rn n} : IsExtremeRay K y ↔ Tdaf.ConvexAnalysis.IsExtremeDirection K y

§18 (p. 162). For a convex cone, extreme rays and extreme directions are the same data.

theorem Rockafellar.isExposedRay_iff_isExposedDirection {n : ℕ} {K : Set (TdafSurface.Rn n)} (hne : K.Nonempty) (hcone : ∀ x ∈ K, ∀ (a : ℝ), 0 ≤ a → a • x ∈ K) {y : TdafSurface.Rn n} : IsExposedRay K y ↔ Tdaf.ConvexAnalysis.IsExposedDirection K y

theorem Rockafellar.forall_smul_mem_of_isCone {n : ℕ} {K : Set (TdafSurface.Rn n)} (hK : IsCone K) (hKcl : IsClosed K) (x : TdafSurface.Rn n) : x ∈ K → ∀ (a : ℝ), 0 ≤ a → a • x ∈ K

A non-empty closed cone in Rockafellar's sense — closed under positive scalar multiplication — is closed under non-negative scaling, which is the form the backbone's cone theorems take.

theorem Rockafellar.corollary_18_5_2 {n : ℕ} {K T : Set (TdafSurface.Rn n)} (hK : Convex ℝ K) (hKcl : IsClosed K) (hcone : IsCone K) (hne : K.Nonempty) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine K) (hTK : T ⊆ K) (hgen : ∀ (y : TdafSurface.Rn n), IsExtremeRay K y → ∃ x ∈ T, ∃ (a : ℝ), 0 < a ∧ y = a • x) : ↑(PointedCone.hull ℝ T) = K

Corollary 18.5.2. If K is a closed convex cone containing no lines and every extreme ray of K is generated by some x ∈ T ⊆ K, then K is the convex cone generated by T. The book's "containing more than just the origin" is unnecessary: the zero cone has no extreme rays, so the hypothesis on T is vacuous and both sides are {0}.

Directions at infinity pass to the recession cone (p. 163)

If C' is a half-line face of a closed convex set C with endpoint x then C' ⊆ x + 0⁺C ⊆ C by Theorem 8.3, so C' - x is an extreme ray of 0⁺C. The converse fails: a parabolic set in ℝ² has no half-line face at all, while its recession cone is a ray.

theorem Rockafellar.subset_extremeDirections_recessionCone {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) : Tdaf.ConvexAnalysis.extremeDirections C ⊆ Tdaf.ConvexAnalysis.extremeDirections (Tdaf.ConvexAnalysis.recessionCone C)

§18 (p. 163). Every extreme direction of a closed convex set C is an extreme direction of 0⁺C — sharper than Theorem 8.3, which gives only that it is a direction of recession.

theorem Rockafellar.subset_exposedDirections_recessionCone {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) : Tdaf.ConvexAnalysis.exposedDirections C ⊆ Tdaf.ConvexAnalysis.exposedDirections (Tdaf.ConvexAnalysis.recessionCone C)

§18 (p. 163). Every exposed direction of a closed convex set C is one of 0⁺C.

theorem Rockafellar.isExtremeRay_recessionCone {n : ℕ} {C : Set (TdafSurface.Rn n)} {y : TdafSurface.Rn n} (hC : Convex ℝ C) (hCcl : IsClosed C) (hy : Tdaf.ConvexAnalysis.IsExtremeDirection C y) : IsExtremeRay (Tdaf.ConvexAnalysis.recessionCone C) y

§18 (p. 163), in the book's own wording: if C' is a half-line face of the closed convex set C with endpoint x, then C' - x is an extreme ray of the cone 0⁺C.

theorem Rockafellar.isExposedRay_recessionCone {n : ℕ} {C : Set (TdafSurface.Rn n)} {y : TdafSurface.Rn n} (hC : Convex ℝ C) (hCcl : IsClosed C) (hy : Tdaf.ConvexAnalysis.IsExposedDirection C y) : IsExposedRay (Tdaf.ConvexAnalysis.recessionCone C) y

Theorem 18.6: Straszewicz's theorem

theorem Rockafellar.theorem_18_6 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) : Set.extremePoints ℝ C ⊆ closure (Set.exposedPoints ℝ C)

Theorem 18.6 (Straszewicz's Theorem). Every extreme point of a closed convex set is the limit of a sequence of exposed points.

theorem Rockafellar.theorem_18_6_closure {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) : Set.exposedPoints ℝ C ⊆ Set.extremePoints ℝ C ∧ closure (Set.exposedPoints ℝ C) = closure (Set.extremePoints ℝ C)

Theorem 18.6 in the book's own phrasing: the exposed points of a closed convex set form a dense subset of its extreme points.

Exposed faces and exposed points (p. 162)

theorem Rockafellar.isExposed_iff_exists_vector {n : ℕ} {C C' : Set (TdafSurface.Rn n)} : IsExposed ℝ C C' ↔ C'.Nonempty → ∃ (b : TdafSurface.Rn n), C' = {x : TdafSurface.Rn n | x ∈ C ∧ ∀ y ∈ C, ((TdafSurface.pairing n) y) b ≤ ((TdafSurface.pairing n) x) b}

§18 (p. 162). The exposed faces of C are the sets of points at which some linear function ⟨·, b⟩ attains its maximum over C. The book's vector b and Mathlib's continuous linear functional are the same quantification in ℝⁿ.

theorem Rockafellar.mem_exposedPoints_iff {n : ℕ} {C : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} : x ∈ Set.exposedPoints ℝ C ↔ x ∈ C ∧ ∃ (b : TdafSurface.Rn n), (∀ y ∈ C, ((TdafSurface.pairing n) y) b ≤ ((TdafSurface.pairing n) x) b) ∧ ∀ y ∈ C, ((TdafSurface.pairing n) x) b ≤ ((TdafSurface.pairing n) y) b → y = x

§18 (p. 162). An exposed point of C is a point through which there is a supporting hyperplane containing no other point of C.

Theorem 18.7: the exposed representation

theorem Rockafellar.theorem_18_7 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine C) : closure (Tdaf.ConvexAnalysis.convexHullPD (Set.exposedPoints ℝ C) (Tdaf.ConvexAnalysis.exposedDirections C)) = C

Theorem 18.7. A closed convex set containing no lines is cl (conv S), for S the set of its exposed points and exposed directions. Unlike Theorem 18.5 the closure cannot be dropped: the exposed points of a closed convex set need not form a closed set.

theorem Rockafellar.corollary_18_7_1 {n : ℕ} {K T : Set (TdafSurface.Rn n)} (hK : Convex ℝ K) (hKcl : IsClosed K) (hcone : IsCone K) (hne : K.Nonempty) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine K) (hTK : T ⊆ K) (hgen : ∀ (y : TdafSurface.Rn n), IsExposedRay K y → ∃ x ∈ T, ∃ (a : ℝ), 0 < a ∧ y = a • x) : closure ↑(PointedCone.hull ℝ T) = K

Corollary 18.7.1. If K is a closed convex cone containing no lines and every exposed ray of K is generated by some x ∈ T ⊆ K, then K is the closure of the convex cone generated by T.

The book prints this corollary with no proof. The argument it wants is the one given for Corollary 18.5.2, one layer up: by Theorem 18.7, K = cl (conv S) for S the exposed points and exposed directions of K; the origin is the only exposed point, being the only extreme point of a line-free cone; and conv of the origin with a set of directions is the cone they generate.

Theorem 18.8: the tangent representation

def Rockafellar.IsTangentHyperplaneAt {n : ℕ} (C : Set (TdafSurface.Rn n)) (b x : TdafSurface.Rn n) : Prop

§18 (p. 168). A hyperplane is tangent to a closed convex set C at x if it is the unique supporting hyperplane to C at x; here it is {z | ⟨z, b⟩ = ⟨x, b⟩}, with tangent half-space {z | ⟨z, b⟩ ≤ ⟨x, b⟩}. IsTangentAt renders "unique hyperplane" as uniqueness of the functional up to a positive multiple: a hyperplane fixes its functional up to a non-zero scalar, and the supporting inequality fixes the sign.

Equations

• Rockafellar.IsTangentHyperplaneAt C b x = Tdaf.ConvexAnalysis.IsTangentAt C (TdafSurface.linFn b) x

theorem Rockafellar.theorem_18_8 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCcl : IsClosed C) (hint : (interior C).Nonempty) : ⋂ (b : TdafSurface.Rn n), ⋂ (x : TdafSurface.Rn n), ⋂ (_ : IsTangentHyperplaneAt C b x), {z : TdafSurface.Rn n | ((TdafSurface.pairing n) z) b ≤ ((TdafSurface.pairing n) x) b} = C

Theorem 18.8. An n-dimensional closed convex set in ℝⁿ is the intersection of the closed half-spaces tangent to it. "n-dimensional in ℝⁿ" is (interior C).Nonempty.