theorem helperForCorollary_19_1_2_pack_transformedEpigraph_from_functionRepresentation {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hk : k ≤ m) (hrepr : ∀ (x : Fin n → ℝ), f x = sInf {r : EReal | ∃ (lam : Fin m → ℝ), (∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) ∧ ∑ i : Fin m with ↑i < k, lam i = 1 ∧ (∀ (i : Fin m), 0 ≤ lam i) ∧ r = ↑(∑ i : Fin m, lam i * α i)}) : IsFinitelyGeneratedConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f)

Helper for Corollary 19.1.2: packing coefficient-representation data into finite generation of the transformed epigraph.

theorem helperForCorollary_19_1_2_exists_fixedCoeffs_of_mem_mixedConvexHull_rangeEarly {n k m : ℕ} (p : Fin k → Fin n → ℝ) (d : Fin m → Fin n → ℝ) {y : Fin n → ℝ} (hy : y ∈ mixedConvexHull (Set.range p) (Set.range d)) : ∃ (a : Fin k → ℝ) (b : Fin m → ℝ), (∀ (i : Fin k), 0 ≤ a i) ∧ (∀ (j : Fin m), 0 ≤ b j) ∧ ∑ i : Fin k, a i = 1 ∧ y = ∑ i : Fin k, a i • p i + ∑ j : Fin m, b j • d j

Helper for Corollary 19.1.2: from mixed-hull membership with finite families, extract fixed-index nonnegative coefficients for the point and direction families.

theorem helperForCorollary_19_1_2_polyhedralFunction_of_epigraphFG {n : ℕ} {f : (Fin n → ℝ) → EReal} (hconv : ConvexFunctionOn Set.univ f) (hfg_epi : IsFinitelyGeneratedConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f)) : IsPolyhedralConvexFunction n f

Helper for Corollary 19.1.2: finite-generation of the transformed epigraph yields a polyhedral convex function.