@[reducible, inline]

noncomputable abbrev supportFunctionEReal {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] (C : Set 𝓗) (u : 𝓗) : EReal

The support function of C evaluated at u, viewed as an EReal supremum of the inner product functional on C.

theorem supportFunctionEReal_eq_sSup_image {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] [CompleteSpace 𝓗] (C : Set 𝓗) (u : 𝓗) : σ[C] u = sSup ((fun (x : 𝓗) => ↑(inner ℝ x u)) '' C)

The support function σ[C] is the supremum of the image of C under the functional x ↦ ⟪x, u⟫.

def supportFunctionHalfspace {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] (C : Set 𝓗) (u : 𝓗) : Set 𝓗

The support halfspace of C in the direction u is the closed halfspace cut out by the support-function bound ⟪x, u⟫ ≤ σ[C] u.

theorem mem_supportFunctionHalfspace_iff {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] [CompleteSpace 𝓗] (C : Set 𝓗) (u x : 𝓗) : x ∈ supportFunctionHalfspace C u ↔ ↑(inner ℝ x u) ≤ σ[C] u

A point belongs to the support halfspace of C in the direction u exactly when its inner product with u is bounded above by the support value σ[C] u.

theorem closure_convexHull_eq_iInter_supportFunctionHalfspace {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] [CompleteSpace 𝓗] (C : Set 𝓗) : closure ((convexHull ℝ) C) = ⋂ (u : 𝓗), supportFunctionHalfspace C u

Proposition 7.11: the closed convex hull of C is the intersection of the support halfspaces cut out by the support function σ[C].