theorem helperForCorollary_19_1_2_mem_of_sInf_eq_real_of_closed {S : Set EReal} {r : ℝ} (hSnonempty : S.Nonempty) (hSclosed : IsClosed S) (hsInf_real : sInf S = ↑r) : ↑r ∈ S

Helper for Corollary 19.1.2: in EReal, if a nonempty closed set has infimum a finite real value, then that value belongs to the set.

theorem helperForCorollary_19_1_2_unpack_mixedHull_generators_for_transformedEpigraph_extractData {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfg_epi : IsFinitelyGeneratedConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f)) : ∃ (k : ℕ) (m : ℕ) (p : Fin k → Fin (n + 1) → ℝ) (d : Fin m → Fin (n + 1) → ℝ), (fun (q : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) q) '' epigraph Set.univ f = mixedConvexHull (Set.range p) (Set.range d)

Helper for Corollary 19.1.2: extract finite indexed point and ray generator families for the transformed epigraph from IsFinitelyGeneratedConvexSet.

theorem helperForCorollary_19_1_2_exists_fixedCoeffs_of_mem_mixedConvexHull_range {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 membership in a mixed convex hull generated by finite families, extract fixed-index coefficient functions on those families.

theorem helperForCorollary_19_1_2_linearImage_mixedConvexHull_range {n p k m : ℕ} (L : (Fin n → ℝ) →ₗ[ℝ] Fin p → ℝ) (pointGen : Fin k → Fin n → ℝ) (dirGen : Fin m → Fin n → ℝ) : ⇑L '' mixedConvexHull (Set.range pointGen) (Set.range dirGen) = mixedConvexHull (Set.range fun (i : Fin k) => L (pointGen i)) (Set.range fun (j : Fin m) => L (dirGen j))

Helper for Corollary 19.1.2: linear maps send mixed convex hulls generated by finite families to mixed convex hulls generated by the mapped families.

theorem helperForCorollary_19_1_2_linearImage_finitelyGeneratedSet {n p : ℕ} {C : Set (Fin n → ℝ)} (hfg : IsFinitelyGeneratedConvexSet n C) (L : (Fin n → ℝ) →ₗ[ℝ] Fin p → ℝ) : IsFinitelyGeneratedConvexSet p (⇑L '' C)

Helper for Corollary 19.1.2: linear images of finitely generated convex sets remain finitely generated.

theorem helperForCorollary_19_1_2_decode_transformedGeneratorCoeffs_to_Text19_0_10_lam {n k' m' : ℕ} (p : Fin k' → Fin (n + 1) → ℝ) (d : Fin m' → Fin (n + 1) → ℝ) {x : Fin n → ℝ} {μ : ℝ} {a' : Fin k' → ℝ} {b' : Fin m' → ℝ} (ha_nonneg : ∀ (i : Fin k'), 0 ≤ a' i) (hb_nonneg : ∀ (j : Fin m'), 0 ≤ b' j) (hsum_a : ∑ i : Fin k', a' i = 1) (hy_repr : (prodLinearEquiv_append_coord n) (x, μ) = ∑ i : Fin k', a' i • p i + ∑ j : Fin m', b' j • d j) : ∃ (lam : Fin (k' + m') → ℝ), (∀ (j0 : Fin n), ∑ i : Fin (k' + m'), lam i * Fin.append (fun (i : Fin k') => ((prodLinearEquiv_append_coord n).symm (p i)).1) (fun (j : Fin m') => ((prodLinearEquiv_append_coord n).symm (d j)).1) i j0 = x j0) ∧ ∑ i : Fin (k' + m') with ↑i < k', lam i = 1 ∧ (∀ (i : Fin (k' + m')), 0 ≤ lam i) ∧ ∑ i : Fin (k' + m'), lam i * Fin.append (fun (i : Fin k') => ((prodLinearEquiv_append_coord n).symm (p i)).2) (fun (j : Fin m') => ((prodLinearEquiv_append_coord n).symm (d j)).2) i = μ

Helper for Corollary 19.1.2: decode fixed-index mixed-hull coefficients in transformed epigraph coordinates into Text 19.0.10 coefficient data.

theorem helperForCorollary_19_1_2_unpack_packGenerators_coeffs_to_Text19_0_10_le {n k' m' : ℕ} (p : Fin k' → Fin (n + 1) → ℝ) (d : Fin m' → Fin (n + 1) → ℝ) {x : Fin n → ℝ} {μ : ℝ} (hy : (prodLinearEquiv_append_coord n) (x, μ) ∈ mixedConvexHull (Set.range p) (Set.range d)) : ∃ (lam : Fin (k' + m') → ℝ) (q : ℝ), (∀ (j0 : Fin n), ∑ i : Fin (k' + m'), lam i * Fin.append (fun (i : Fin k') => ((prodLinearEquiv_append_coord n).symm (p i)).1) (fun (j : Fin m') => ((prodLinearEquiv_append_coord n).symm (d j)).1) i j0 = x j0) ∧ ∑ i : Fin (k' + m') with ↑i < k', lam i = 1 ∧ (∀ (i : Fin (k' + m')), 0 ≤ lam i) ∧ q ≤ μ ∧ q = ∑ i : Fin (k' + m'), lam i * Fin.append (fun (i : Fin k') => ((prodLinearEquiv_append_coord n).symm (p i)).2) (fun (j : Fin m') => ((prodLinearEquiv_append_coord n).symm (d j)).2) i

Helper for Corollary 19.1.2: decode mixed-hull membership in packed transformed-epigraph coordinates into feasible Text 19.0.10 coefficients with an objective value bounded by μ.

theorem helperForCorollary_19_1_2_unpack_packedMembership_to_Text19_0_10_le {n k' m' : ℕ} (p : Fin k' → Fin (n + 1) → ℝ) (d : Fin m' → Fin (n + 1) → ℝ) {x : Fin n → ℝ} {μ : ℝ} (hy : (prodLinearEquiv_append_coord n) (x, μ) ∈ mixedConvexHull (Set.range p) (Set.range d)) : ∃ (lam : Fin (k' + m') → ℝ), (∀ (j0 : Fin n), ∑ i : Fin (k' + m'), lam i * Fin.append (fun (i : Fin k') => ((prodLinearEquiv_append_coord n).symm (p i)).1) (fun (j : Fin m') => ((prodLinearEquiv_append_coord n).symm (d j)).1) i j0 = x j0) ∧ ∑ i : Fin (k' + m') with ↑i < k', lam i = 1 ∧ (∀ (i : Fin (k' + m')), 0 ≤ lam i) ∧ ∑ i : Fin (k' + m'), ↑(lam i) * ↑(Fin.append (fun (i : Fin k') => ((prodLinearEquiv_append_coord n).symm (p i)).2) (fun (j : Fin m') => ((prodLinearEquiv_append_coord n).symm (d j)).2) i) ≤ ↑μ

Helper for Corollary 19.1.2: unpack packed transformed-epigraph mixed-hull membership into feasible decoded coefficients with objective value bounded above by μ.

theorem helperForCorollary_19_1_2_unpack_mixedHull_generators_for_transformedEpigraph_transport_feasible {n k' m' : ℕ} (p : Fin k' → Fin (n + 1) → ℝ) (d : Fin m' → Fin (n + 1) → ℝ) {x : Fin n → ℝ} {lam : Fin (k' + m') → ℝ} (hlin : ∀ (j0 : Fin n), ∑ i : Fin (k' + m'), lam i * Fin.append (fun (i : Fin k') => ((prodLinearEquiv_append_coord n).symm (p i)).1) (fun (j : Fin m') => ((prodLinearEquiv_append_coord n).symm (d j)).1) i j0 = x j0) (hnorm : ∑ i : Fin (k' + m') with ↑i < k', lam i = 1) (hnonneg : ∀ (i : Fin (k' + m')), 0 ≤ lam i) : (prodLinearEquiv_append_coord n) (x, ∑ i : Fin (k' + m'), lam i * Fin.append (fun (i : Fin k') => ((prodLinearEquiv_append_coord n).symm (p i)).2) (fun (j : Fin m') => ((prodLinearEquiv_append_coord n).symm (d j)).2) i) ∈ mixedConvexHull (Set.range p) (Set.range d)

Helper for Corollary 19.1.2: feasible decoded Text 19.0.10 coefficients transport to membership in the mixed convex hull generated by transformed epigraph families.

theorem helperForCorollary_19_1_2_unpack_mixedHull_generators_for_transformedEpigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfg_epi : IsFinitelyGeneratedConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f)) : ∃ (k : ℕ) (m : ℕ) (a : Fin m → Fin n → ℝ) (α : Fin m → ℝ), k ≤ m ∧ ∀ (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)}

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

theorem helperForCorollary_19_1_2_finitelyGeneratedFunction_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)) : IsFinitelyGeneratedConvexFunction n f

Helper for Corollary 19.1.2: finite-generation of the transformed epigraph induces finite-generation of the function representation.

theorem helperForCorollary_19_1_2_epigraphFG_of_finitelyGeneratedFunction {n : ℕ} {f : (Fin n → ℝ) → EReal} : IsFinitelyGeneratedConvexFunction n f → IsFinitelyGeneratedConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f)

Helper for Corollary 19.1.2: finite-generation of the function representation induces finite-generation of the transformed epigraph.

theorem helperForCorollary_19_1_2_polyhedral_imp_finitelyGenerated {n : ℕ} {f : (Fin n → ℝ) → EReal} : IsPolyhedralConvexFunction n f → IsFinitelyGeneratedConvexFunction n f

Helper for Corollary 19.1.2: polyhedral convex functions are finitely generated.

theorem helperForCorollary_19_1_2_finitelyGenerated_imp_polyhedral {n : ℕ} {f : (Fin n → ℝ) → EReal} : IsFinitelyGeneratedConvexFunction n f → IsPolyhedralConvexFunction n f

Helper for Corollary 19.1.2: finitely generated convex functions are polyhedral.

theorem helperForCorollary_19_1_2_closed_of_polyhedral_proper {n : ℕ} {f : (Fin n → ℝ) → EReal} : IsPolyhedralConvexFunction n f → ProperConvexFunctionOn Set.univ f → ClosedConvexFunction f

Helper for Corollary 19.1.2: a proper polyhedral convex function is closed.

theorem helperForCorollary_19_1_2_nonempty_of_sInf_eq_real {S : Set EReal} {r : ℝ} (hr : sInf S = ↑r) : S.Nonempty

Helper for Corollary 19.1.2: an EReal infimum equal to a finite real value cannot come from the empty set.