theorem helperForTheorem_19_2_extractFiniteRepresentation {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfpoly : IsPolyhedralConvexFunction n 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 Theorem 19.2: extract a finite Text 19.0.10 representation from polyhedrality.

theorem helperForTheorem_19_2_kZero_forces_constTop {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hk0 : k = 0) (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)}) (x : Fin n → ℝ) : f x = ⊤

Helper for Theorem 19.2: in a Text 19.0.10 representation, k = 0 forces f = ⊤.

theorem helperForTheorem_19_2_kZero_forces_constTop_and_conjugate_constNegInf {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hk0 : k = 0) (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)}) : fenchelConjugate n f = constNegInf n

Helper for Theorem 19.2: the degenerate k = 0 branch gives fenchelConjugate n f = constNegInf n.

theorem helperForTheorem_19_2_constNegInf_isPolyhedralConvexFunction (n : ℕ) : IsPolyhedralConvexFunction n (constNegInf n)

Helper for Theorem 19.2: the constant -∞ function is polyhedral convex.

theorem helperForTheorem_19_2_existsPointIndex_of_posK {k m : ℕ} (hkpos : 0 < k) (hk : k ≤ m) : ∃ (i0 : Fin m), ↑i0 < k

Helper for Theorem 19.2: positivity of k and k ≤ m provides a point-index below k.

theorem helperForTheorem_19_2_value_le_of_feasibleCoefficients {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin 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)}) {x : Fin n → ℝ} {lam : Fin m → ℝ} (hlin : ∀ (j : Fin n), ∑ i : Fin m, lam i * a i j = x j) (hnorm : ∑ i : Fin m with ↑i < k, lam i = 1) (hnonneg : ∀ (i : Fin m), 0 ≤ lam i) : f x ≤ ↑(∑ i : Fin m, lam i * α i)

Helper for Theorem 19.2: any feasible coefficient vector gives an upper bound on the represented function value.

theorem helperForTheorem_19_2_generatorValue_le_alpha {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin 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)}) (i : Fin m) (hi : ↑i < k) : f (a i) ≤ ↑(α i)

Helper for Theorem 19.2: each point-generator value is bounded above by its coefficient value.

theorem helperForTheorem_19_2_pointBounds_of_conjugateLe {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin 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)}) {xStar : Fin n → ℝ} {μ : ℝ} (hconj : fenchelConjugate n f xStar ≤ ↑μ) (i : Fin m) : ↑i < k → a i ⬝ᵥ xStar - α i ≤ μ

Helper for Theorem 19.2: a finite upper bound on the conjugate yields the point-generator inequalities.

theorem helperForTheorem_19_2_finiteBounds_of_conjugateLe {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hkpos : 0 < k) (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)}) {xStar : Fin n → ℝ} {μ : ℝ} (hconj : fenchelConjugate n f xStar ≤ ↑μ) : (∀ (i : Fin m), ↑i < k → a i ⬝ᵥ xStar - α i ≤ μ) ∧ ∀ (i : Fin m), k ≤ ↑i → a i ⬝ᵥ xStar - α i ≤ 0

Helper for Theorem 19.2: finite conjugate sublevel bounds imply the two finite generator inequality families (point and direction).

theorem helperForTheorem_19_2_conjugateLe_of_finiteBounds {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hkpos : 0 < k) (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)}) {xStar : Fin n → ℝ} {μ : ℝ} (hpoint : ∀ (i : Fin m), ↑i < k → a i ⬝ᵥ xStar - α i ≤ μ) (hdir : ∀ (i : Fin m), k ≤ ↑i → a i ⬝ᵥ xStar - α i ≤ 0) : fenchelConjugate n f xStar ≤ ↑μ

Helper for Theorem 19.2: finite point and direction generator bounds imply the corresponding finite upper bound for the conjugate.

theorem helperForTheorem_19_2_conjugate_le_iff_finiteGeneratorBounds {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hkpos : 0 < k) (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)}) {xStar : Fin n → ℝ} {μ : ℝ} : fenchelConjugate n f xStar ≤ ↑μ ↔ (∀ (i : Fin m), ↑i < k → a i ⬝ᵥ xStar - α i ≤ μ) ∧ ∀ (i : Fin m), k ≤ ↑i → a i ⬝ᵥ xStar - α i ≤ 0

Helper for Theorem 19.2: conjugate sublevel membership is equivalent to the two finite generator-bound families.

theorem helperForTheorem_19_2_memTransformedEpigraphCoord_iff_bounds {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hkpos : 0 < k) (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)}) (y : Fin (n + 1) → ℝ) : y ∈ (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ (fenchelConjugate n f) ↔ (∀ (i : Fin m), ↑i < k → a i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1 - α i ≤ ((prodLinearEquiv_append_coord n).symm y).2) ∧ ∀ (i : Fin m), k ≤ ↑i → a i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1 - α i ≤ 0

Helper for Theorem 19.2: transformed-epigraph membership is equivalent to the finite generator-bound families at the pulled-back pair coordinates.

theorem helperForTheorem_19_2_prodLinearEquivAppendCoord_castSucc {n : ℕ} (x0 : Fin n → ℝ) (μ0 : ℝ) (j0 : Fin n) : x0 j0 = (prodLinearEquiv_append_coord n) (x0, μ0) j0.castSucc

Helper for Theorem 19.2: packed-coordinate dot products with (a i, -1) decode to the affine expression dotProduct (a i) x - μ.

theorem helperForTheorem_19_2_prodLinearEquivAppendCoord_last {n : ℕ} (x0 : Fin n → ℝ) (μ0 : ℝ) : μ0 = (prodLinearEquiv_append_coord n) (x0, μ0) (Fin.last n)

Helper for Theorem 19.2: the last packed coordinate is the appended scalar.

theorem helperForTheorem_19_2_dotProduct_prodLinearEquivAppendCoord {n : ℕ} (p q : (Fin n → ℝ) × ℝ) : (prodLinearEquiv_append_coord n) p ⬝ᵥ (prodLinearEquiv_append_coord n) q = p.1 ⬝ᵥ q.1 + p.2 * q.2

Helper for Theorem 19.2: dot product in packed coordinates splits into the base dot product plus the product of appended scalar coordinates.

theorem helperForTheorem_19_2_dotPacked_point {n m : ℕ} {a : Fin m → Fin n → ℝ} (i : Fin m) (y : Fin (n + 1) → ℝ) : y ⬝ᵥ (prodLinearEquiv_append_coord n) (a i, -1) = a i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1 - ((prodLinearEquiv_append_coord n).symm y).2

Helper for Theorem 19.2: packed-coordinate dot products with (a i, -1) decode to the affine expression dotProduct (a i) x - μ.

theorem helperForTheorem_19_2_dotPacked_direction {n m : ℕ} {a : Fin m → Fin n → ℝ} (i : Fin m) (y : Fin (n + 1) → ℝ) : y ⬝ᵥ (prodLinearEquiv_append_coord n) (a i, 0) = a i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1

Helper for Theorem 19.2: packed-coordinate dot products with (a i, 0) decode to dotProduct (a i) x.

theorem helperForTheorem_19_2_pointBoundsCoord_polyhedral {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} : IsPolyhedralConvexSet (n + 1) {y : Fin (n + 1) → ℝ | ∀ (i : Fin m), ↑i < k → a i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1 - α i ≤ ((prodLinearEquiv_append_coord n).symm y).2}

Helper for Theorem 19.2: the point-generator bound family in transformed coordinates is a polyhedral convex set.

theorem helperForTheorem_19_2_directionBoundsCoord_polyhedral {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} : IsPolyhedralConvexSet (n + 1) {y : Fin (n + 1) → ℝ | ∀ (i : Fin m), k ≤ ↑i → a i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1 - α i ≤ 0}

Helper for Theorem 19.2: the direction-generator bound family in transformed coordinates is a polyhedral convex set.

theorem helperForTheorem_19_2_transformedEpigraphCoord_eq_pointDirInter {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hkpos : 0 < k) (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)}) : (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ (fenchelConjugate n f) = {y : Fin (n + 1) → ℝ | ∀ (i : Fin m), ↑i < k → a i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1 - α i ≤ ((prodLinearEquiv_append_coord n).symm y).2} ∩ {y : Fin (n + 1) → ℝ | ∀ (i : Fin m), k ≤ ↑i → a i ⬝ᵥ ((prodLinearEquiv_append_coord n).symm y).1 - α i ≤ 0}

Helper for Theorem 19.2: the transformed epigraph of the conjugate equals the intersection of the point- and direction-bound coordinate sets.

theorem helperForTheorem_19_2_polyhedralTransformedEpigraph_of_conjugate {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hkpos : 0 < k) (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)}) : IsPolyhedralConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ (fenchelConjugate n f))

Helper for Theorem 19.2: in the nondegenerate branch, the transformed epigraph of the conjugate is polyhedral.

theorem helperForTheorem_19_2_nondegenerate_branch_polyhedralConjugate {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} (hkpos : 0 < k) (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)}) : IsPolyhedralConvexFunction n (fenchelConjugate n f)

Helper for Theorem 19.2: the nondegenerate representation branch (0 < k) already yields polyhedrality of the Fenchel conjugate.

theorem polyhedralConvexFunction_fenchelConjugate (n : ℕ) (f : (Fin n → ℝ) → EReal) : IsPolyhedralConvexFunction n f → IsPolyhedralConvexFunction n (fenchelConjugate n f)

Theorem 19.2: The conjugate of a polyhedral convex function is polyhedral.