def IsFace {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C C' : Set E) : Prop

Defn 18.1 (the face of a convex set). Let C be a convex set. A subset C' ⊆ C is a face of C if, for every closed line segment in C, whenever the relative interior of the segment (i.e. the open segment) is contained in C', then both endpoints of the segment belong to C'.

Equations

• IsFace C C' = (Convex 𝕜 C ∧ IsExtreme 𝕜 C C')

theorem openSegment_nonempty_of_exists_pos_add_eq_one {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (hcoeff : ∃ (a : 𝕜) (b : 𝕜), 0 < a ∧ 0 < b ∧ a + b = 1) (x y : E) : (openSegment 𝕜 x y).Nonempty

A positive pair of coefficients summing to 1 yields a nonempty open segment.

theorem isFace_empty {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) (hC : Convex 𝕜 C) : IsFace C ∅

Text 18.0.1 (empty set is a face of itself). Let C be a convex set. The empty set ∅ is a face of C.

theorem isFace_self {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) (hC : Convex 𝕜 C) : IsFace C C

Text 18.0.2 (convex set is a face of itself). Let C be a convex set. The set C itself is a face of C.

def IsExtremePoint {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) (x : E) : Prop

Defn 18.2 (the extreme point of a convex set). A point x ∈ C is an extreme point of C if there is no nontrivial way to write x as a convex combination (1 - λ) y + λ z with y ∈ C, z ∈ C and 0 < λ < 1, except by taking y = z = x. Equivalently, x belongs to no open segment with endpoints in C unless both endpoints are x.

Equations

• IsExtremePoint C x = (x ∈ C ∧ ∀ ⦃y z : E⦄, y ∈ C → z ∈ C → x ∈ openSegment 𝕜 y z → y = x ∧ z = x)

theorem isExtremePoint_iff_mem_extremePoints {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) (x : E) : IsExtremePoint C x ↔ x ∈ Set.extremePoints 𝕜 C

Defn 18.2 (the extreme point of a convex set): the book definition is equivalent to membership in the mathlib set of extreme points C.extremePoints 𝕜.

theorem isFace_singleton_iff_isExtremePoint {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) (x : E) : IsFace C {x} ↔ Convex 𝕜 C ∧ IsExtremePoint C x

Text 18.0.3 (zero-dimensional faces are extreme points). The zero-dimensional faces of a convex set C (informally: singleton faces {x}) are equivalent to the extreme points of C.

def IsExtremeRay {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (K : ConvexCone 𝕜 E) (R : Set E) : Prop

Defn 18.3 (extreme ray). For a convex cone, an extreme ray is a face that is a half-line emanating from the origin; equivalently, it is a face of the form {t • x | t ≥ 0} for some nonzero vector x.

Equations

• IsExtremeRay K R = (IsFace (↑K) R ∧ ∃ (x : E), x ≠ 0 ∧ R = (fun (t : 𝕜) => t • x) '' Set.Ici 0)

def IsDirectionOf {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C' : Set E) (d : E) : Prop

Defn 18.4 (extreme direction). If C' is a half-line face of a convex set C, the direction of C' is called an extreme direction of C (an “extreme point of C at infinity”).

This helper predicate says that d is a (nonzero) direction vector of a half-line set C', meaning C' can be parameterized as x + t • d for t ≥ 0.

Equations

• IsDirectionOf C' d = ∃ (x : E), d ≠ 0 ∧ C' = (fun (t : 𝕜) => x + t • d) '' Set.Ici 0

def IsHalfLineFace {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C C' : Set E) : Prop

Defn 18.4 (half-line face). A half-line face of a convex set C is a face C' of C that is a half-line (ray) in the ambient space.

Equations

• IsHalfLineFace C C' = (IsFace C C' ∧ ∃ (d : E), IsDirectionOf C' d)

def IsExtremeDirection {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) (d : E) : Prop

Defn 18.4 (extreme direction). A vector d is an extreme direction of a convex set C if it is the direction of some half-line face C' of C.

Equations

• IsExtremeDirection C d = ∃ (C' : Set E), IsHalfLineFace C C' ∧ IsDirectionOf C' d

def maximizers {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C : Set F) (h : F →ₗ[ℝ] ℝ) : Set F

Text 18.0.5 (Properties of the set of maximizers). Let C be a convex set in ℝⁿ and let h be a linear functional. Define C' as the set of points where h attains its maximum over C, so C' = {x ∈ C | h x = α} where α = sup_C h.

Equations

• maximizers C h = {x : F | x ∈ C ∧ IsMaxOn (fun (x : F) => h x) C x}

theorem mem_maximizers_iff {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C : Set F} {h : F →ₗ[ℝ] ℝ} {x : F} : x ∈ maximizers C h ↔ x ∈ C ∧ ∀ y ∈ C, h y ≤ h x

Membership in the set of maximizers amounts to being in C and maximizing h on C.

theorem h_eq_of_mem_maximizers {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C : Set F} {h : F →ₗ[ℝ] ℝ} {x y : F} (hx : x ∈ maximizers C h) (hy : y ∈ maximizers C h) : h x = h y

Any two maximizers have the same objective value.

theorem mem_maximizers_of_mem_of_eq_value {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C : Set F} {h : F →ₗ[ℝ] ℝ} {x x' : F} (hx : x ∈ maximizers C h) (hx'C : x' ∈ C) (hxeq : h x' = h x) : x' ∈ maximizers C h

A point in C with the same value as a maximizer is itself a maximizer.

theorem h_convexCombo_eq_max {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C : Set F} {h : F →ₗ[ℝ] ℝ} {x y : F} {a b : ℝ} (hx : x ∈ maximizers C h) (hy : y ∈ maximizers C h) (hab : a + b = 1) : h (a • x + b • y) = h x

Linear functionals agree on convex combinations of maximizers.

theorem convex_maximizers {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C : Set F) (h : F →ₗ[ℝ] ℝ) (hC : Convex ℝ C) : Convex ℝ (maximizers C h)

Text 18.0.5 (Properties of the set of maximizers): the set of maximizers of a linear functional on a convex set is convex.

theorem h_eq_endpoints_of_mem_openSegment_of_mem_maximizers {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C : Set F} {h : F →ₗ[ℝ] ℝ} {x y z : F} (hx : x ∈ C) (hy : y ∈ C) (hz : z ∈ openSegment ℝ x y) (hzmax : z ∈ maximizers C h) : h x = h z ∧ h y = h z

A maximizer inside an open segment forces equal endpoint values.

theorem mem_maximizers_endpoints_of_mem_openSegment {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C : Set F} {h : F →ₗ[ℝ] ℝ} {x y z : F} (hx : x ∈ C) (hy : y ∈ C) (hz : z ∈ openSegment ℝ x y) (hzmax : z ∈ maximizers C h) : x ∈ maximizers C h ∧ y ∈ maximizers C h

Endpoints of an open segment containing a maximizer are maximizers.

theorem segment_subset_maximizers_of_mem_openSegment {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C : Set F) (h : F →ₗ[ℝ] ℝ) (hC : Convex ℝ C) {x y z : F} (hx : x ∈ C) (hy : y ∈ C) (hz : z ∈ openSegment ℝ x y) (hzmax : z ∈ maximizers C h) : segment ℝ x y ⊆ maximizers C h

Text 18.0.5 (Properties of the set of maximizers): if a maximizer lies in the relative interior of a line segment in C, then every point of that segment is a maximizer.

theorem isFace_maximizers {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C : Set F) (h : F →ₗ[ℝ] ℝ) (hC : Convex ℝ C) : IsFace C (maximizers C h)

Text 18.0.6. Let C be a convex set and let h be a linear functional. Let α = sup_{x ∈ C} h x. If α < ∞, define the set of maximizers C' = {x ∈ C | h x = α}. Then C' is a face of C.

def IsExposedFace {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C Face : Set F) : Prop

Defn 18.5 (Exposed face, directions and rays). Let C be a convex set. A subset F ⊆ C is an exposed face of C if there exists a linear functional h (coming from a supporting hyperplane) such that F is exactly the set of maximizers of h over C, i.e. F = {x ∈ C | h x = sup_{y ∈ C} h y}.

The exposed directions of C (exposed points at infinity) are the direction vectors of exposed half-line faces of C.

An exposed ray of a convex cone is an exposed face which is a half-line emanating from the origin.

Equations

• IsExposedFace C Face = (Convex ℝ C ∧ Face ⊆ C ∧ ∃ (h : F →ₗ[ℝ] ℝ), Face = maximizers C h)

theorem maximizers_eq_inter_levelset_of_le_of_exists_eq {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C : Set F} {h : F →ₗ[ℝ] ℝ} {a : ℝ} (hle : ∀ x ∈ C, h x ≤ a) (hex : ∃ x ∈ C, h x = a) : maximizers C h = C ∩ {x : F | h x = a}

Maximizers with an attained upper bound are exactly a level set.

theorem maximizers_zero_eq {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C : Set F) : maximizers C 0 = C

Maximizers of the zero functional are the whole set.

theorem isExposedFace_iff_exists_supportingHyperplane {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C Face : Set F) (hC : Convex ℝ C) (hFace_nonempty : Face.Nonempty) (hFace_proper : Face ⊂ C) : IsExposedFace C Face ↔ ∃ (h : F →ₗ[ℝ] ℝ) (a : ℝ), h ≠ 0 ∧ (∀ x ∈ C, h x ≤ a) ∧ (∃ x ∈ C, h x = a) ∧ Face = C ∩ {x : F | h x = a}

Text 18.0.7. Let C be a convex set. A nonempty proper subset Face ⊂ C is an exposed face of C if and only if there exists a nontrivial supporting hyperplane H to C such that Face = C ∩ H.

def IsExposedPoint {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C : Set F) (x : F) : Prop

Defn 18.5 (exposed point). A point x ∈ C is an exposed point of a convex set C if the singleton face {x} is an exposed face of C (i.e. {x} is the set of maximizers of some linear functional on C).

Equations

• IsExposedPoint C x = IsExposedFace C {x}

theorem isExtremePoint_of_isExposedPoint {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C : Set F) {x : F} (hx : IsExposedPoint C x) : IsExtremePoint C x

Text 18.0.8. Let C be a convex set. If x ∈ C is an exposed point, then x is an extreme point of C.

def IsExposedHalfLineFace {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C C' : Set F) : Prop

Defn 18.5 (exposed half-line face). A half-line face C' of a convex set C is exposed if it is an exposed face of C (equivalently: it is the set of maximizers of some linear functional over C).

Equations

• IsExposedHalfLineFace C C' = (IsHalfLineFace C C' ∧ IsExposedFace C C')

def IsExposedDirection {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C : Set F) (d : F) : Prop

Defn 18.5 (exposed direction). A vector d is an exposed direction of a convex set C if it is the direction of some exposed half-line face of C.

Equations

• IsExposedDirection C d = ∃ (C' : Set F), IsExposedHalfLineFace C C' ∧ IsDirectionOf C' d

def exposedDirections {F : Type u_3} [AddCommGroup F] [Module ℝ F] (C : Set F) : Set F

Text 18.0.9. The exposed directions (exposed points at infinity) of a convex set C are defined to be the directions of the exposed half-line faces of C.

Equations

• exposedDirections C = {d : F | IsExposedDirection C d}

def IsExposedRay {F : Type u_3} [AddCommGroup F] [Module ℝ F] (K : ConvexCone ℝ F) (R : Set F) : Prop

Defn 18.5 (exposed ray). A set R is an exposed ray of a convex cone K if it is an exposed face of K and it is a half-line of the form {t • x | t ≥ 0} for some nonzero x.

Equations

• IsExposedRay K R = (IsExposedFace (↑K) R ∧ ∃ (x : F), x ≠ 0 ∧ R = (fun (t : ℝ) => t • x) '' Set.Ici 0)

theorem isExtremeRay_of_isExposedRay {F : Type u_3} [AddCommGroup F] [Module ℝ F] (K : ConvexCone ℝ F) (R : Set F) (hR : IsExposedRay K R) : IsExtremeRay K R

Text 18.0.10. Let R be an exposed ray of a convex set C (typically defined via the recession cone 0⁺ C). Then R is an extreme ray.

In this file we formulate the statement for an exposed ray of a convex cone K (e.g. K = 0⁺ C), showing that every exposed ray is an extreme ray.

@[reducible, inline]

abbrev exampleC : Set (EuclideanSpace ℝ (Fin 3))

The example set in ℝ³ used to exhibit a non-exposed extreme point.

Equations

• exampleC = {x : EuclideanSpace ℝ (Fin 3) | x.ofLp 2 = 0 ∧ max (x.ofLp 0) 0 ^ 2 ≤ x.ofLp 1}

theorem max_sq_le_convex_comb {x y a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : max (a * x + b * y) 0 ^ 2 ≤ a * max x 0 ^ 2 + b * max y 0 ^ 2

A convex-combination bound for r ↦ (max r 0)^2.

theorem convex_exampleC : Convex ℝ exampleC

The example set exampleC is convex.

theorem isExtremePoint_origin_exampleC : IsExtremePoint exampleC 0

The origin is an extreme point of exampleC.

theorem not_isExposedPoint_origin_exampleC : ¬IsExposedPoint exampleC 0

The origin is not an exposed point of exampleC.

theorem exists_isExtremePoint_not_isExposedPoint : ∃ (C : Set (EuclideanSpace ℝ (Fin 3))) (x : EuclideanSpace ℝ (Fin 3)), Convex ℝ C ∧ IsExtremePoint C x ∧ ¬IsExposedPoint C x

Text 18.0.11 (Not every extreme point is an exposed point). In general, an extreme point of a convex set need not be an exposed point. A concrete example is obtained by taking C to be the convex hull of a torus in ℝ³: if D is the flat disk forming the “top” face of C, then any point on the relative boundary (rim) of D is an extreme point of C but is not an exposed point of C.

theorem isFace_trans {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {C C' C'' : Set E} (hC' : IsFace C C') (hC'' : IsFace C' C'') : IsFace C C''

Text 18.0.12 (Transitivity of Faces). Let C be a convex set.

(1) If C'' is a face of C' and C' is a face of C, then C'' is a face of C.

(2) In particular, if x is an extreme point of a face C' of C, then x is an extreme point of C.

theorem isExtremePoint_of_isFace_of_isExtremePoint {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {C C' : Set E} {x : E} (hC' : IsFace C C') (hx : IsExtremePoint C' x) : IsExtremePoint C x

theorem isFace_of_isFace_of_subset {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {C C' D : Set E} (hC' : IsFace C C') (hD : Convex 𝕜 D) (hC'D : C' ⊆ D) (hDC : D ⊆ C) : IsFace D C'

Text 18.0.13. If C' is a face of C, and D is a convex set satisfying C' ⊆ D ⊆ C, then C' is also a face of D.

theorem mem_openSegment_of_point_beyond {n : ℕ} {x z y : EuclideanSpace ℝ (Fin n)} {t : ℝ} (ht : 0 < t) (hy : y = z + t • (z - x)) : z ∈ openSegment ℝ x y

If t > 0 and y = z + t • (z - x), then z is in the open segment from x to y.

theorem exists_mem_openSegment_of_mem_euclideanRelativeInterior {n : ℕ} {D : Set (EuclideanSpace ℝ (Fin n))} {z x : EuclideanSpace ℝ (Fin n)} (hz : z ∈ euclideanRelativeInterior n D) (hx : x ∈ D) (hxz : x ≠ z) : ∃ y ∈ D, z ∈ openSegment ℝ x y

From z ∈ ri D and x ∈ D, x ≠ z, build y ∈ D with z in the open segment x–y.

theorem subset_of_isFace_of_convex_of_euclideanRelativeInterior_inter {n : ℕ} {C C' D : Set (EuclideanSpace ℝ (Fin n))} (hC' : IsFace C C') (hDC : D ⊆ C) (hri : (euclideanRelativeInterior n D ∩ C').Nonempty) : D ⊆ C'

Theorem 18.1. Let C be a convex set, and let C' be a face of C. If D is a convex set in C such that ri D meets C', then D ⊆ C'.

theorem euclideanRelativeInterior_nonempty_of_convex_of_nonempty {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hC : Convex ℝ C) (hCne : C.Nonempty) : (euclideanRelativeInterior n C).Nonempty

Relative interior of a nonempty convex set in ℝⁿ is nonempty.

theorem euclideanRelativeInterior_mono_of_subset_of_affineSpan_eq {n : ℕ} {A B : Set (EuclideanSpace ℝ (Fin n))} (hAB : A ⊆ B) (haff : affineSpan ℝ A = affineSpan ℝ B) : euclideanRelativeInterior n A ⊆ euclideanRelativeInterior n B

Relative interior is monotone under inclusion when affine spans coincide.

theorem affineSpan_inter_closure_eq_affineSpan {n : ℕ} {C C' : Set (EuclideanSpace ℝ (Fin n))} (hC' : C' ⊆ C) : affineSpan ℝ (C ∩ closure C') = affineSpan ℝ C'

The affine span of C ∩ closure C' equals the affine span of C' when C' ⊆ C.

theorem isFace_eq_inter_closure {n : ℕ} {C C' : Set (EuclideanSpace ℝ (Fin n))} (hC' : IsFace C C') (hC'conv : Convex ℝ C') : C' = C ∩ closure C'

Corollary 18.1.1. If C' is a face of a convex set C, then C' = C ∩ closure C'. In particular, if C is closed, then C' is closed.

theorem isClosed_of_isFace {n : ℕ} {C C' : Set (EuclideanSpace ℝ (Fin n))} (hC' : IsFace C C') (hC'conv : Convex ℝ C') (hC : IsClosed C) : IsClosed C'

Corollary 18.1.1. If C' is a face of a closed convex set C, then C' is closed.

theorem subset_of_isFace_of_isFace_of_ri_inter {n : ℕ} {C C' D : Set (EuclideanSpace ℝ (Fin n))} (hC' : IsFace C C') (hD : IsFace C D) (hri : (euclideanRelativeInterior n D ∩ C').Nonempty) : D ⊆ C'

If C' and D are faces of C and ri D meets C', then D ⊆ C'.

theorem isFace_eq_of_euclideanRelativeInterior_inter {n : ℕ} {C C' C'' : Set (EuclideanSpace ℝ (Fin n))} (hC' : IsFace C C') (hC'' : IsFace C C'') (hri : (euclideanRelativeInterior n C' ∩ euclideanRelativeInterior n C'').Nonempty) : C' = C''

Corollary 18.1.2. If C' and C'' are faces of a convex set C such that ri C' and ri C'' have a point in common, then actually C' = C''.

theorem isFace_eq_of_euclideanRelativeInterior_inter_self {n : ℕ} {C C' : Set (EuclideanSpace ℝ (Fin n))} (hC' : IsFace C C') (hri : (euclideanRelativeInterior n C ∩ C').Nonempty) : C' = C

If ri C meets a face C', then C' = C.

theorem isFace_subset_euclideanRelativeBoundary_of_ne {n : ℕ} {C C' : Set (EuclideanSpace ℝ (Fin n))} (hC' : IsFace C C') (hne : C' ≠ C) : C' ⊆ euclideanRelativeBoundary n C

Corollary 18.1.3. Let C be a convex set, and let C' be a face of C other than C itself. Then C' is entirely contained in the relative boundary of C.

theorem finrank_direction_affineSpan_lt_of_isFace_ne {n : ℕ} {C C' : Set (EuclideanSpace ℝ (Fin n))} (hC' : IsFace C C') (hne : C' ≠ C) (hC'conv : Convex ℝ C') (hC'ne : C'.Nonempty) (hCne : C.Nonempty) : Module.finrank ℝ ↥(affineSpan ℝ C').direction < Module.finrank ℝ ↥(affineSpan ℝ C).direction

Corollary 18.1.3. Let C be a convex set, and let C' be a face of C other than C itself. Then dim C' < dim C (formalized as a strict inequality between the finranks of the directions of the affine spans of C' and C).

def FaceOf {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) : Type u_2

The type of faces of a set C, using the predicate IsFace (𝕜 := 𝕜) C.

Equations

• FaceOf C = { C' : Set E // IsFace C C' }

instance FaceOf.instPartialOrder {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) : PartialOrder (FaceOf C)

Faces are ordered by inclusion of their carriers.

Equations

• FaceOf.instPartialOrder C = { le := fun (F G : FaceOf C) => ↑F ⊆ ↑G, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

def FaceOf.sInf {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) (hC : Convex 𝕜 C) (S : Set (FaceOf C)) : FaceOf C

The infimum of a set of faces, defined by intersecting all faces (and C).

Equations

• FaceOf.sInf C hC S = ⟨⋂ (i : Option { F : FaceOf C // F ∈ S }), match i with | none => C | some F => ↑↑F, ⋯⟩

theorem FaceOf.isGLB_sInf {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (C : Set E) (hC : Convex 𝕜 C) (S : Set (FaceOf C)) : IsGLB S (sInf C hC S)

The infimum defined above is a greatest lower bound.

theorem faces_completeLattice {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) : ∃ (inst : CompleteLattice (FaceOf C)), ∀ (F G : FaceOf C), F ≤ G ↔ ↑F ⊆ ↑G

Text 18.1.1 (Lattice Structure of Faces). Let C be a convex set in ℝⁿ, and let 𝓕(C) be the collection of all faces of C. Ordered by set inclusion ⊆, 𝓕(C) is a complete lattice. Moreover, every strictly decreasing chain of faces in 𝓕(C) has finite length (equivalently: there is no infinite strictly decreasing sequence of faces).

theorem not_exists_faces_strictlyDecreasingChain {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) : ¬∃ (f : ℕ → Set (EuclideanSpace ℝ (Fin n))), (∀ (k : ℕ), IsFace C (f k)) ∧ (∀ (k : ℕ), Convex ℝ (f k)) ∧ ∀ (k : ℕ), f (k + 1) ⊂ f k

Text 18.1.1 (Lattice Structure of Faces): there is no infinite strictly decreasing chain of faces of a convex set (formulated as the nonexistence of a sequence f : ℕ → Set of faces with f (k+1) ⊂ f k for all k).

theorem maximizers_eq_inter_of_subset_of_nonempty {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C D : Set F} (h : F →ₗ[ℝ] ℝ) (hDC : D ⊆ C) (hmax : maximizers C h ⊆ D) (hnonempty : (maximizers C h).Nonempty) : maximizers D h = maximizers C h ∩ D

If D ⊆ C contains all maximizers of h on C, then the maximizers on D are exactly the maximizers on C, provided the maximizers on C are nonempty.

theorem isExposedFace_of_isExposedFace_of_subset {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C C' D : Set F} (hC' : IsExposedFace C C') (hC'nonempty : C'.Nonempty) (hD : Convex ℝ D) (hC'D : C' ⊆ D) (hDC : D ⊆ C) : IsExposedFace D C'

Text 18.0.13. If C' is exposed in C, and D is a convex set satisfying C' ⊆ D ⊆ C, then C' is also exposed in D (assuming C' is nonempty).

theorem smul_mem_recessionCone_of_mem {E : Type u_3} [AddCommGroup E] [Module ℝ E] {C : Set E} {y : E} (hy : y ∈ C.recessionCone) {t : ℝ} (ht : 0 ≤ t) : t • y ∈ C.recessionCone

Nonnegative scaling preserves membership in a recession cone.

theorem mem_recessionCone_of_isExtremeDirection {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCclosed : IsClosed C) {d : EuclideanSpace ℝ (Fin n)} (hd : IsExtremeDirection C d) : d ∈ C.recessionCone

An extreme direction yields a recession direction for closed convex sets in ℝⁿ.

theorem isExtremeDirection_recessionCone_of_isExtremeDirection {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (hCclosed : IsClosed C) {d : EuclideanSpace ℝ (Fin n)} (hd : IsExtremeDirection C d) : IsExtremeDirection C.recessionCone d

Text 18.0.14. Every extreme direction (and every exposed direction) of a closed convex set C is also an extreme direction (respectively: exposed direction) of the recession cone 0⁺ C (formalized as Set.recessionCone C); however, the converse implication does not hold in general.

theorem isExtremeDirection_of_isExposedDirection {F : Type u_3} [AddCommGroup F] [Module ℝ F] {C : Set F} {d : F} (hd : IsExposedDirection C d) : IsExtremeDirection C d

Exposed directions are extreme directions.

@[reducible, inline]

abbrev parabolaSet : Set (EuclideanSpace ℝ (Fin 2))

The parabola epigraph in ℝ².

Equations

• parabolaSet = {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 1 ≥ x.ofLp 0 ^ 2}

@[reducible, inline]

abbrev verticalDir : EuclideanSpace ℝ (Fin 2)

The vertical direction in ℝ².

Equations

• verticalDir = !₂[0, 1]

theorem convex_parabola_set : Convex ℝ parabolaSet

The parabola epigraph is convex.

theorem parabola_no_vertical_halfLineFace {x0 : EuclideanSpace ℝ (Fin 2)} {C' : Set (EuclideanSpace ℝ (Fin 2))} (hC' : C' = (fun (t : ℝ) => x0 + t • verticalDir) '' Set.Ici 0) : ¬IsFace parabolaSet C'

The parabola epigraph has no vertical half-line faces.

theorem exists_isExtremeDirection_recessionCone_not_isExtremeDirection : ∃ (C : Set (EuclideanSpace ℝ (Fin 2))) (d : EuclideanSpace ℝ (Fin 2)), IsClosed C ∧ Convex ℝ C ∧ IsExtremeDirection C.recessionCone d ∧ ¬IsExtremeDirection C d

Text 18.0.14 (converse fails for extreme directions). There exists a closed convex set C and a vector d such that d is an extreme direction of 0⁺ C but not an extreme direction of C.