theorem helperForCorollary_19_1_2_sInf_coe_image_eq_sInf_real {T : Set ℝ} (hT_nonempty : T.Nonempty) (hT_bddBelow : BddBelow T) : sInf ((fun (q : ℝ) => ↑q) '' T) = ↑(sInf T)

Helper for Corollary 19.1.2: coercing a nonempty lower-bounded real set into EReal preserves its infimum.

theorem helperForCorollary_19_1_2_exists_lam_of_nonemptyObjectiveSet {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} {x : Fin n → ℝ} (hSnonempty : {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)}.Nonempty) : ∃ (lam : Fin m → ℝ) (r : EReal), (∀ (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: nonemptiness of the objective-value set gives one admissible coefficient vector.

theorem helperForCorollary_19_1_2_objectiveValueSet_eq_image_feasibleCoefficients {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} {x : Fin n → ℝ} : {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 (lam : Fin m → ℝ) => ↑(∑ i : Fin m, lam i * α i)) '' {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}

Helper for Corollary 19.1.2: the objective-value set equals the image of the feasible coefficient set under the linear objective map (cast to EReal).

theorem helperForCorollary_19_1_2_objectiveValueMap_continuous {m : ℕ} {α : Fin m → ℝ} : Continuous fun (lam : Fin m → ℝ) => ↑(∑ i : Fin m, lam i * α i)

Helper for Corollary 19.1.2: continuity of the coefficient objective map into EReal.

theorem helperForCorollary_19_1_2_objectiveValueSet_closed_of_compactFeasible {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} {x : Fin n → ℝ} (hcompact_feasible : IsCompact {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}) : IsClosed {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: compactness of the feasible coefficient set implies closedness of the objective-value set.

theorem helperForCorollary_19_1_2_closed_objectiveValueSet_of_feasibleFG {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} {x : Fin n → ℝ} (hfg_feasible : IsFinitelyGeneratedConvexSet m {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}) : IsClosed {q : ℝ | ∃ (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) ∧ q = ∑ i : Fin m, lam i * α i}

Helper for Corollary 19.1.2: finite generation of the feasible coefficient set implies closedness of the associated objective-value set.

theorem helperForCorollary_19_1_2_feasibleCoeffSet_finitelyGenerated {n k m : ℕ} {a : Fin m → Fin n → ℝ} {x : Fin n → ℝ} : IsFinitelyGeneratedConvexSet m {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}

Helper for Corollary 19.1.2: the feasible coefficient set for fixed x is finitely generated because it is the solution set of finitely many linear equalities and inequalities.

theorem helperForCorollary_19_1_2_closed_objectiveValueSet {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} {x : Fin n → ℝ} : IsClosed {q : ℝ | ∃ (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) ∧ q = ∑ i : Fin m, lam i * α i}

Helper for Corollary 19.1.2: closedness of the objective-value set attached to one finitely generated representation at fixed x.

theorem helperForCorollary_19_1_2_memObjectiveSet_of_finiteValue {n k m : ℕ} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} {x : Fin n → ℝ} {r : ℝ} (hsInf_real : 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)} = ↑r) : ↑r ∈ {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: if the infimum of the objective-value set is a finite real, then that real value belongs to the objective-value set.

theorem helperForCorollary_19_1_2_attainment_value_of_infMember {n k m : ℕ} {f : (Fin n → ℝ) → EReal} {a : Fin m → Fin n → ℝ} {α : Fin m → ℝ} {x : Fin n → ℝ} {r : ℝ} (hrfx : f x = ↑r) (hrmem : ↑r ∈ {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)}) : ∃ (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) ∧ f x = ↑(∑ i : Fin m, lam i * α i)

Helper for Corollary 19.1.2: membership of the finite infimum value in the objective set gives coefficients attaining exactly f x.

theorem helperForCorollary_19_1_2_attainment_of_finiteValue {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 → ℝ) : (∃ (r : ℝ), f x = ↑r) → ∃ (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) ∧ f x = ↑(∑ i : Fin m, lam i * α i)

Helper for Corollary 19.1.2: in a fixed finite-generation representation, finite values are attained by admissible coefficients.

theorem helperForCorollary_19_1_2_unpackData_with_attainment {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfgen : IsFinitelyGeneratedConvexFunction 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)}) ∧ ∀ (x : Fin n → ℝ), (∃ (r : ℝ), f x = ↑r) → ∃ (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) ∧ f x = ↑(∑ i : Fin m, lam i * α i)

Helper for Corollary 19.1.2: a finitely generated representation can be unpacked into coefficients data together with pointwise attainment for every finite value.

theorem polyhedral_convex_iff_finitelyGenerated_and_closed_and_attainment (n : ℕ) (f : (Fin n → ℝ) → EReal) : (IsPolyhedralConvexFunction n f ↔ IsFinitelyGeneratedConvexFunction n f) ∧ (IsPolyhedralConvexFunction n f → ProperConvexFunctionOn Set.univ f → ClosedConvexFunction f) ∧ (IsFinitelyGeneratedConvexFunction 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)}) ∧ ∀ (x : Fin n → ℝ), (∃ (r : ℝ), f x = ↑r) → ∃ (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) ∧ f x = ↑(∑ i : Fin m, lam i * α i))

Corollary 19.1.2: A convex function is polyhedral iff it is finitely generated; such a function, if proper, is closed; and in the finitely generated representation the infimum at x, when finite, is attained by some coefficients λ.

theorem helperForText_19_0_11_signedSum_le_absSum {n : ℕ} (x : Fin n → ℝ) (σ : Fin n → Bool) : (∑ j : Fin n, x j * if σ j = true then 1 else -1) ≤ ∑ j : Fin n, |x j|

Helper for Text 19.0.11: every signed sum is bounded above by the ℓ¹ value.

theorem helperForText_19_0_11_exists_sign_attains_absSum {n : ℕ} (x : Fin n → ℝ) : ∃ (σ : Fin n → Bool), (∑ j : Fin n, x j * if σ j = true then 1 else -1) = ∑ j : Fin n, |x j|

Helper for Text 19.0.11: choosing coordinate-wise signs attains the ℓ¹ value.

theorem helperForText_19_0_11_sSup_signedValues_eq_absSum {n : ℕ} (x : Fin n → ℝ) : sSup {r : ℝ | ∃ (σ : Fin n → Bool), r = ∑ j : Fin n, x j * if σ j = true then 1 else -1} = ∑ j : Fin n, |x j|

Helper for Text 19.0.11: the supremum over all signed linear forms equals ∑ |x i|.

theorem polyhedralConvex_absSum (n : ℕ) : IsPolyhedralConvexFunction n fun (x : Fin n → ℝ) => ↑(∑ i : Fin n, |x i|)

Text 19.0.11: The function f(x) = |ξ₁| + ··· + |ξₙ| on ℝ^n is polyhedral convex, since it is the pointwise supremum of the 2^n linear functions x ↦ ε₁ ξ₁ + ··· + εₙ ξₙ with εⱼ ∈ {+1, -1}.

theorem polyhedralConvex_tchebycheffSupNorm (n : ℕ) : IsPolyhedralConvexFunction n fun (x : Fin n → ℝ) => ↑(sSup {r : ℝ | ∃ (i : Fin n), r = |x i|})

Text 19.0.12: The Tchebycheff (supremum) norm f : ℝ^n → ℝ defined by f(x) = max {|ξ₁|, …, |ξₙ|} (with x = (ξ₁, …, ξₙ)) is polyhedral convex, since it is the pointwise supremum of the 2n linear functions x ↦ ε_j ξ_j with ε_j ∈ {+1, -1} for j = 1, …, n.

theorem helperForText_19_0_13_affineLine_x1_eq_one_data : ∃ (L : AffineSubspace ℝ (Fin 2 → ℝ)), Module.finrank ℝ ↥L.direction = 1 ∧ ↑L = {x : Fin 2 → ℝ | x 1 = 1} ∧ 0 ∉ ↑L

Helper for Text 19.0.13: build an explicit affine line in ℝ² with equation x 1 = 1 and record that the origin is not on it.

theorem helperForText_19_0_13_lineSet_polyhedral : IsPolyhedralConvexSet 2 {x : Fin 2 → ℝ | x 1 = 1}

Helper for Text 19.0.13: the explicit line {x | x 1 = 1} is polyhedral convex.

theorem helperForText_19_0_13_originSingleton_polyhedral : IsPolyhedralConvexSet 2 {0}

Helper for Text 19.0.13: the singleton containing the origin in ℝ² is polyhedral convex.

theorem helperForText_19_0_13_notClosed_convexHull_line_union_origin : ¬IsClosed ((convexHull ℝ) ({x : Fin 2 → ℝ | x 1 = 1} ∪ {0}))

Helper for Text 19.0.13: the convex hull of the line {x | x 1 = 1} united with {0} is not closed.

theorem helperForText_19_0_13_notPolyhedral_convexHull_line_union_origin : ¬IsPolyhedralConvexSet 2 ((convexHull ℝ) ({x : Fin 2 → ℝ | x 1 = 1} ∪ {0}))

Helper for Text 19.0.13: the same convex hull is therefore not polyhedral.

theorem exists_polyhedralConvexSets_convexHull_union_not_polyhedral : ∃ (C₁ : Set (Fin 2 → ℝ)) (C₂ : Set (Fin 2 → ℝ)), IsPolyhedralConvexSet 2 C₁ ∧ IsPolyhedralConvexSet 2 C₂ ∧ ¬IsPolyhedralConvexSet 2 ((convexHull ℝ) (C₁ ∪ C₂))

Text 19.0.13: The convex hull of the union of two polyhedral convex sets need not be polyhedral; for instance, this occurs for a line and a point not on the line.

theorem helperForText_19_0_14_compact_of_polytope {n : ℕ} {C : Set (Fin n → ℝ)} (hCpoly : IsPolytope n C) : IsCompact C

Helper for Text 19.0.14: every polytope in ℝ^n is compact.

theorem helperForText_19_0_14_shift_eq_zero_of_compact_translateInvariant {n : ℕ} {C : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hCcompact : IsCompact C) (hCnonempty : C.Nonempty) (htranslate : C + {d} = C) : d = 0

Helper for Text 19.0.14: a nonempty compact set in ℝ^n invariant under translation by d must satisfy d = 0.

theorem helperForText_19_0_14_unique_translation_parameter {n : ℕ} {C S : Set (Fin n → ℝ)} {y₀ y : Fin n → ℝ} (hSnonempty : S.Nonempty) (hSC : S ⊆ C) (hCcompact : IsCompact C) (hy₀ : S + {y₀} = C) (hy : S + {y} = C) : y = y₀

Helper for Text 19.0.14: if two translates of S both equal C, then the translation vectors coincide.

theorem helperForText_19_0_14_polytope_of_empty_or_singleton (n : ℕ) : IsPolytope n ∅ ∧ ∀ (y₀ : Fin n → ℝ), IsPolytope n {y₀}

Helper for Text 19.0.14: both the empty set and every singleton in ℝ^n are polytopes.

theorem helperForText_19_0_14_eq_singleton_of_mem_and_unique {α : Type u_1} {D : Set α} {y₀ : α} (hy₀D : y₀ ∈ D) (hunique : ∀ y ∈ D, y = y₀) : D = {y₀}

Helper for Text 19.0.14: a set equals a singleton once it contains the center point and every element equals that point.

theorem polytope_setOf_translate_eq (n : ℕ) (C S : Set (Fin n → ℝ)) : IsPolytope n C → S.Nonempty → S ⊆ C → IsPolytope n {y : Fin n → ℝ | S + {y} = C}

Text 19.0.14: Let C ⊆ ℝ^n be a convex polytope and let S ⊆ C be nonempty. For y ∈ ℝ^n, define the translate S + {y} and D := {y | S + {y} = C}. Then D is a possibly empty convex polytope in ℝ^n.