theorem closedConvex_eq_empty_of_extremePoints_eq_empty {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) (hExt : Set.extremePoints ℝ C = ∅) : C = ∅

A closed convex set with no lines and no extreme points must be empty.

theorem extremePoints_nonempty_of_closedConvex_noLines {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) (hCne : C.Nonempty) : (Set.extremePoints ℝ C).Nonempty

Corollary 18.5.3. A nonempty closed convex set containing no lines has an extreme point.

def text18_5_2_C1 : Set (EuclideanSpace ℝ (Fin 3))

The closed unit disk in the xy-plane.

Equations

• text18_5_2_C1 = {v : EuclideanSpace ℝ (Fin 3) | v.ofLp 2 = 0 ∧ v.ofLp 0 ^ 2 + v.ofLp 1 ^ 2 ≤ 1}

def text18_5_2_C2 : Set (EuclideanSpace ℝ (Fin 3))

The vertical segment through (1,0,0) of length 2.

Equations

• text18_5_2_C2 = {v : EuclideanSpace ℝ (Fin 3) | v.ofLp 0 = 1 ∧ v.ofLp 1 = 0 ∧ |v.ofLp 2| ≤ 1}

def text18_5_2_S : Set (EuclideanSpace ℝ (Fin 3))

The base set for the convex hull.

Equations

• text18_5_2_S = text18_5_2_C1 ∪ text18_5_2_C2

def text18_5_2_C : Set (EuclideanSpace ℝ (Fin 3))

The convex closed hull used in the construction.

Equations

• text18_5_2_C = (closedConvexHull ℝ) text18_5_2_S

def text18_5_2_p : EuclideanSpace ℝ (Fin 3)

The midpoint of the vertical segment.

Equations

• text18_5_2_p = !₂[1, 0, 0]

def text18_5_2_zTop : EuclideanSpace ℝ (Fin 3)

The top endpoint of the vertical segment.

Equations

• text18_5_2_zTop = !₂[1, 0, 1]

def text18_5_2_zBot : EuclideanSpace ℝ (Fin 3)

The bottom endpoint of the vertical segment.

Equations

• text18_5_2_zBot = !₂[1, 0, -1]

def text18_5_2_y (n : ℕ) : ℝ

The auxiliary scalar sequence yₙ = 1/(n+2).

Equations

• text18_5_2_y n = 1 / (↑n + 2)

def text18_5_2_q (n : ℕ) : EuclideanSpace ℝ (Fin 3)

The auxiliary sequence of points on the circle in the xy-plane.

Equations

• text18_5_2_q n = !₂[√(1 - text18_5_2_y n ^ 2), text18_5_2_y n, 0]

theorem text18_5_2_y_pos (n : ℕ) : 0 < text18_5_2_y n

The auxiliary sequence yₙ is positive.

theorem text18_5_2_y_sq_lt_one (n : ℕ) : text18_5_2_y n ^ 2 < 1

The auxiliary sequence satisfies yₙ^2 < 1.

theorem text18_5_2_q_mem_C1 (n : ℕ) : text18_5_2_q n ∈ text18_5_2_C1

The point qₙ lies on the boundary circle of C1.

theorem text18_5_2_norm_sq_eq (v : EuclideanSpace ℝ (Fin 3)) : ‖v‖ ^ 2 = v.ofLp 0 ^ 2 + v.ofLp 1 ^ 2 + v.ofLp 2 ^ 2

Expand the squared norm in ℝ³ as the sum of squares of coordinates.

theorem text18_5_2_C1_subset_closedBall_one : text18_5_2_C1 ⊆ Metric.closedBall 0 1

The disk C1 is contained in the closed unit ball.

theorem text18_5_2_C1_subset_closedBall : text18_5_2_C1 ⊆ Metric.closedBall 0 2

The disk C1 is contained in a closed ball of radius 2.

theorem text18_5_2_C2_subset_closedBall : text18_5_2_C2 ⊆ Metric.closedBall 0 2

The segment C2 is contained in a closed ball of radius 2.

theorem text18_5_2_C_def_and_basic_props : IsClosed text18_5_2_C ∧ Bornology.IsBounded text18_5_2_C ∧ Convex ℝ text18_5_2_C

Basic properties of the convex closed hull C.

theorem text18_5_2_p_not_mem_extremePoints : text18_5_2_p ∉ Set.extremePoints ℝ text18_5_2_C

The midpoint of the vertical segment is not an extreme point of C.

theorem text18_5_2_y_tendsto_zero : Filter.Tendsto text18_5_2_y Filter.atTop (nhds 0)

The auxiliary sequence yₙ tends to 0.

theorem text18_5_2_tendsto_q : Filter.Tendsto text18_5_2_q Filter.atTop (nhds text18_5_2_p)

The auxiliary sequence of points on the circle converges to p.

theorem text18_5_2_q0_lt_one (n : ℕ) : √(1 - text18_5_2_y n ^ 2) < 1

The x-coordinate of qₙ is strictly less than 1.

theorem text18_5_2_q_norm (n : ℕ) : ‖text18_5_2_q n‖ = 1

The point qₙ has norm 1.

theorem text18_5_2_mem_convexHull_S_decomp {v : EuclideanSpace ℝ (Fin 3)} (hv : v ∈ (convexHull ℝ) text18_5_2_S) : ∃ t ∈ Set.Icc 0 1, ∃ u ∈ (convexHull ℝ) text18_5_2_C1, ∃ w ∈ (convexHull ℝ) text18_5_2_C2, v = (1 - t) • u + t • w

Any point in the convex hull of S splits into a two-piece convex combination.

theorem text18_5_2_q_inner_le_q0_on_convexHull_C2 (n : ℕ) (v : EuclideanSpace ℝ (Fin 3)) : v ∈ (convexHull ℝ) text18_5_2_C2 → inner ℝ (text18_5_2_q n) v ≤ √(1 - text18_5_2_y n ^ 2)

On the convex hull of C2, the supporting functional is at most qₙ's x-coordinate.

theorem text18_5_2_q_inner_le_one_on_C (n : ℕ) (v : EuclideanSpace ℝ (Fin 3)) : v ∈ text18_5_2_C → inner ℝ (text18_5_2_q n) v ≤ 1

The supporting functional is bounded by 1 on C.

theorem text18_5_2_eq_of_mem_C_and_inner_eq_one (n : ℕ) (v : EuclideanSpace ℝ (Fin 3)) : v ∈ text18_5_2_C → inner ℝ (text18_5_2_q n) v = 1 → v = text18_5_2_q n

Points of C attaining the maximum of the supporting functional are exactly qₙ.

theorem text18_5_2_q_mem_exposedPoints (n : ℕ) : text18_5_2_q n ∈ Set.exposedPoints ℝ text18_5_2_C

Each point qₙ is an exposed point of C.

theorem text18_5_2_q_mem_extremePoints (n : ℕ) : text18_5_2_q n ∈ Set.extremePoints ℝ text18_5_2_C

Each point qₙ is an extreme point of C.

theorem text18_5_2_limit_point_in_closure_extremePoints : text18_5_2_p ∈ closure (Set.extremePoints ℝ text18_5_2_C)

A sequence of extreme points approaches p, so extremePoints is not closed.

theorem exists_closed_bounded_convex_extremePoints_not_isClosed : ∃ (C : Set (EuclideanSpace ℝ (Fin 3))), IsClosed C ∧ Bornology.IsBounded C ∧ Convex ℝ C ∧ ¬IsClosed (Set.extremePoints ℝ C)

Text 18.5.2 (Non-Closedness of the Set of Extreme Points). There exists a closed and bounded (hence compact) convex set C ⊆ ℝ³ such that the set of its extreme points ext(C) (formalized as C.extremePoints ℝ) is not closed.