Main inequality: linear functionals bounded by vertex maximum

theorem lemma_1_15_linear_max_at_vertex {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E →ₗ[ℝ] ℝ) (S : Finset E) (hS : S.Nonempty) (x : E) (hx : x ∈ (convexHull ℝ) ↑S) : f x ≤ S.sup' hS ⇑f

Lemma 1.15 (Inequality form). A linear functional on the convex hull of a finite set of vertices is bounded above by the maximum of the functional over the vertices.

For any x ∈ convexHull ℝ S, we have f x ≤ S.sup' hS f.

Corollary: existence of an optimal vertex

theorem lemma_1_15_exists_vertex {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E →ₗ[ℝ] ℝ) (S : Finset E) (x : E) (hx : x ∈ (convexHull ℝ) ↑S) : ∃ v ∈ S, f x ≤ f v

Lemma 1.15 (Vertex existence form). For any point x in the convex hull of a finite set S, there exists a vertex v ∈ S such that f x ≤ f v.

Equality form: supremum over convex hull equals maximum over vertices

theorem lemma_1_15_sSup_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E →ₗ[ℝ] ℝ) (S : Finset E) (hS : S.Nonempty) : sSup (⇑f '' (convexHull ℝ) ↑S) = S.sup' hS ⇑f

Lemma 1.15 (Supremum equality form). The supremum of a linear functional over the convex hull of a finite set equals the maximum (sup') over the set itself:

sSup (f '' convexHull ℝ ↑S) = S.sup' hS f