theorem section13_dotProduct_le_norm_mul_sum_abs {n : ℕ} (x y : Fin n → ℝ) : x ⬝ᵥ y ≤ ‖x‖ * ∑ i : Fin n, |y i|

A crude upper bound for the dot product in terms of the sup norm.

theorem section13_supportFunctionEReal_ne_bot_of_nonempty {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (xStar : Fin n → ℝ) : supportFunctionEReal C xStar ≠ ⊥

A nonempty set has a support function that never takes the value ⊥.

theorem section13_supportFunctionEReal_ne_top_of_isBounded {n : ℕ} {C : Set (Fin n → ℝ)} (hCbd : Bornology.IsBounded C) (xStar : Fin n → ℝ) : supportFunctionEReal C xStar ≠ ⊤

A bounded set has a support function that never takes the value ⊤.

theorem section13_isBounded_of_supportFunctionEReal_finite {n : ℕ} {C : Set (Fin n → ℝ)} (hfinite : ∀ (xStar : Fin n → ℝ), supportFunctionEReal C xStar ≠ ⊤ ∧ supportFunctionEReal C xStar ≠ ⊥) : Bornology.IsBounded C

If the support function of a nonempty set is finite everywhere, then the set is bounded.

theorem section13_closedProper_of_convex_finite {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) (hfinite : ∀ (x : Fin n → ℝ), f x ≠ ⊤ ∧ f x ≠ ⊥) : ClosedConvexFunction f ∧ ProperConvexFunctionOn Set.univ f

A convex function finite everywhere is automatically closed and proper.

theorem exists_supportFunctionEReal_iff_boundedConvex_posHom_finite {n : ℕ} (f : (Fin n → ℝ) → EReal) : (∃ (C : Set (Fin n → ℝ)), C.Nonempty ∧ Convex ℝ C ∧ Bornology.IsBounded C ∧ f = supportFunctionEReal C) ↔ ConvexFunction f ∧ PositivelyHomogeneous f ∧ ∀ (x : Fin n → ℝ), f x ≠ ⊤ ∧ f x ≠ ⊥

Corollary 13.2.2. The support functions of the non-empty bounded convex sets are the finite positively homogeneous convex functions.