theorem k_zero_eq_zero {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {k : (Fin n → ℝ) → EReal} (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hk : ∀ (i : Fin m) (y : Fin n → ℝ), k y = sSup {r : EReal | ∃ (x : Fin n → ℝ), r = f i (x + y) - f i x}) (hm : 0 < m) : k 0 = 0

The common recession function vanishes at the origin.

theorem zero_one_mem_recessionCone_convexHull_union_epigraph {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {k : (Fin n → ℝ) → EReal} (hclosed : ∀ (i : Fin m), ClosedConvexFunction (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hk : ∀ (i : Fin m) (y : Fin n → ℝ), k y = sSup {r : EReal | ∃ (x : Fin n → ℝ), r = f i (x + y) - f i x}) (hm : 0 < m) : have C0 := (convexHull ℝ) (⋃ (i : Fin m), epigraph Set.univ (f i)); (0, 1) ∈ C0.recessionCone

The vertical direction (0,1) lies in the recession cone of the convex hull.

theorem epigraph_convexHullFunctionFamily_eq_convexHull {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hsubset : (convexHull ℝ) (⋃ (i : Fin m), epigraph Set.univ (f i)) ⊆ epigraph Set.univ (convexHullFunctionFamily f)) (hclosed : IsClosed ((convexHull ℝ) (⋃ (i : Fin m), epigraph Set.univ (f i)))) (hrec : (0, 1) ∈ ((convexHull ℝ) (⋃ (i : Fin m), epigraph Set.univ (f i))).recessionCone) : epigraph Set.univ (convexHullFunctionFamily f) = (convexHull ℝ) (⋃ (i : Fin m), epigraph Set.univ (f i))

The convex-hull epigraph is an actual epigraph for the convex-hull function family.

theorem convexHullFunctionFamily_ne_bot {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {k : (Fin n → ℝ) → EReal} (hclosed : ∀ (i : Fin m), ClosedConvexFunction (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hk : ∀ (i : Fin m) (y : Fin n → ℝ), k y = sSup {r : EReal | ∃ (x : Fin n → ℝ), r = f i (x + y) - f i x}) (hm : 0 < m) : have fconv := convexHullFunctionFamily f; ∀ (x : Fin n → ℝ), fconv x ≠ ⊥

The convex-hull function family is never ⊥.

theorem convexHullFunctionFamily_closed_proper_recession_and_attained {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {k : (Fin n → ℝ) → EReal} (hclosed : ∀ (i : Fin m), ClosedConvexFunction (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hk : ∀ (i : Fin m) (y : Fin n → ℝ), k y = sSup {r : EReal | ∃ (x : Fin n → ℝ), r = f i (x + y) - f i x}) (hm : 0 < m) : have fconv := convexHullFunctionFamily f; ClosedConvexFunction fconv ∧ ProperConvexFunctionOn Set.univ fconv ∧ (∀ (y : Fin n → ℝ), k y = sSup {r : EReal | ∃ (x : Fin n → ℝ), r = fconv (x + y) - fconv x}) ∧ ∀ (x : Fin n → ℝ), ∃ (lam : Fin m → ℝ) (x' : Fin m → Fin n → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 ∧ ∑ i : Fin m, lam i • x' i = x ∧ fconv x = ∑ i : Fin m, ↑(lam i) * f i (x' i)

Corollary 9.8.3 9.8.3.1. Let f₁, …, fₘ be closed proper convex functions on ℝ^n all having the same recession function k. Then f = conv {f₁, …, fₘ} is closed and proper and likewise has k as its recession function. In the formula for f(x) in Theorem 5.6, the infimum is attained for each x by some convex combination.