theorem helperForTheorem_19_4_splitRealUpperBound {n : ℕ} {f₁ f₂ : (Fin n → ℝ) → EReal} (hproper₁ : ProperConvexFunctionOn Set.univ f₁) (hproper₂ : ProperConvexFunctionOn Set.univ f₂) {x : Fin n → ℝ} {μ : ℝ} (hsum : f₁ x + f₂ x ≤ ↑μ) : ∃ (μ₁ : ℝ) (μ₂ : ℝ), f₁ x ≤ ↑μ₁ ∧ f₂ x ≤ ↑μ₂ ∧ μ₁ + μ₂ = μ

Helper for Theorem 19.4: split a finite upper bound on f₁ x + f₂ x into real upper bounds for each summand.

theorem helperForTheorem_19_4_addUpperBounds {n : ℕ} {f₁ f₂ : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ₁ μ₂ : ℝ} (hμ₁ : f₁ x ≤ ↑μ₁) (hμ₂ : f₂ x ≤ ↑μ₂) : f₁ x + f₂ x ≤ ↑(μ₁ + μ₂)

Helper for Theorem 19.4: add two real-valued epigraph bounds in EReal.

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

Helper for Theorem 19.4: identify the Fin.castSucc coordinates of prodLinearEquiv_append_coord.

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

Helper for Theorem 19.4: identify the Fin.last coordinate of prodLinearEquiv_append_coord.

theorem polyhedralConvexFunction_add_of_proper (n : ℕ) (f₁ f₂ : (Fin n → ℝ) → EReal) : IsPolyhedralConvexFunction n f₁ → IsPolyhedralConvexFunction n f₂ → ProperConvexFunctionOn Set.univ f₁ → ProperConvexFunctionOn Set.univ f₂ → IsPolyhedralConvexFunction n fun (x : Fin n → ℝ) => f₁ x + f₂ x

Theorem 19.4: If f₁ and f₂ are proper polyhedral convex functions, then f₁ + f₂ is polyhedral.

theorem helperForTheorem_19_5_smul_polyhedral_of_polyhedral {n : ℕ} {C : Set (Fin n → ℝ)} (hCpoly : IsPolyhedralConvexSet n C) (a : ℝ) : IsPolyhedralConvexSet n (a • C)

Helper for Theorem 19.5: scalar multiples of a polyhedral convex set are polyhedral.

theorem helperForTheorem_19_5_mixedConvexHull_nonempty_of_nonempty_of_eq {n : ℕ} {C S₀ S₁ : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCeq : C = mixedConvexHull S₀ S₁) : (mixedConvexHull S₀ S₁).Nonempty

Helper for Theorem 19.5: if a nonempty set is represented as a mixed convex hull, that mixed convex hull is nonempty.

theorem helperForTheorem_19_5_directionHull_subset_recessionCone_of_mixedHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} : mixedConvexHull {0} S₁ ⊆ (mixedConvexHull S₀ S₁).recessionCone

Helper for Theorem 19.5: the mixed hull generated by {0} and S₁ sits in the recession cone of mixedConvexHull S₀ S₁.

theorem helperForTheorem_19_5_pointsNonempty_of_nonempty_mixedConvexHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} (hMixedNonempty : (mixedConvexHull S₀ S₁).Nonempty) : S₀.Nonempty

Helper for Theorem 19.5: a nonempty mixed convex hull must have at least one point-generator.

theorem helperForTheorem_19_5_recessionCone_cone_eq_cone {n : ℕ} {S₁ : Set (Fin n → ℝ)} : (cone n S₁).recessionCone = cone n S₁

Helper for Theorem 19.5: the recession cone of cone S₁ equals cone S₁.

theorem helperForTheorem_19_5_recessionCone_conv_add_cone_of_finite_points {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} (hS₀fin : S₀.Finite) (hS₁fin : S₁.Finite) (hS₀ne : S₀.Nonempty) : (conv S₀ + cone n S₁).recessionCone = cone n S₁

Helper for Theorem 19.5: with finite nonempty point-generators, the recession cone of conv S₀ + cone S₁ is exactly cone S₁.

theorem helperForTheorem_19_5_recessionCone_subset_directionHull_of_finiteMixedHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} (hS₀fin : S₀.Finite) (hS₁fin : S₁.Finite) (hS₀ne : S₀.Nonempty) : (mixedConvexHull S₀ S₁).recessionCone ⊆ mixedConvexHull {0} S₁

Helper for Theorem 19.5: for finite mixed-hull data, every recession direction lies in the mixed hull generated by {0} and the direction set.

theorem helperForTheorem_19_5_recessionCone_eq_directionHull_of_finiteMixedHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} (hS₀fin : S₀.Finite) (hS₁fin : S₁.Finite) (hS₀ne : S₀.Nonempty) : (mixedConvexHull S₀ S₁).recessionCone = mixedConvexHull {0} S₁

Helper for Theorem 19.5: finite mixed-hull representations satisfy 0⁺(mixedConvexHull S₀ S₁) = mixedConvexHull {0} S₁.

theorem helperForTheorem_19_5_recessionCone_polyhedral_of_polyhedral {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCpoly : IsPolyhedralConvexSet n C) : IsPolyhedralConvexSet n C.recessionCone

Helper for Theorem 19.5: the recession cone of a nonempty polyhedral convex set is polyhedral.

theorem polyhedralConvexSet_smul_recessionCone_and_representation (n : ℕ) (C : Set (Fin n → ℝ)) : C.Nonempty → IsPolyhedralConvexSet n C → (∀ (a : ℝ), IsPolyhedralConvexSet n (a • C)) ∧ IsPolyhedralConvexSet n C.recessionCone ∧ ∀ (S₀ S₁ : Set (Fin n → ℝ)), S₀.Finite → S₁.Finite → C = mixedConvexHull S₀ S₁ → C.recessionCone = mixedConvexHull {0} S₁

Theorem 19.5: Let C be a non-empty polyhedral convex set. Then λ • C is polyhedral for every scalar λ, the recession cone 0^+ C is polyhedral, and if C is represented as a mixed convex hull of a finite set of points and directions, then 0^+ C is the mixed convex hull of the origin together with the directions.

theorem helperForCorollary_19_5_1_convexFunctionOn_of_polyhedralTransformedEpigraph {n : ℕ} {g : (Fin n → ℝ) → EReal} (hpoly : IsPolyhedralConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ g)) : ConvexFunctionOn Set.univ g

Helper for Corollary 19.5.1: polyhedrality of the transformed epigraph implies convexity of the corresponding function.

theorem helperForCorollary_19_5_1_polyhedralConvexFunction_of_polyhedralTransformedEpigraph {n : ℕ} {g : (Fin n → ℝ) → EReal} (hpoly : IsPolyhedralConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ g)) : IsPolyhedralConvexFunction n g

Helper for Corollary 19.5.1: packaging transformed-epigraph polyhedrality as IsPolyhedralConvexFunction.

theorem helperForCorollary_19_5_1_recessionCone_transformedEpigraph_eq_transformedEpigraph_recessionFunction {n : ℕ} {f : (Fin n → ℝ) → EReal} (hconv : ConvexFunctionOn Set.univ f) (hproper : ProperConvexFunctionOn Set.univ f) : ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ f).recessionCone = (fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ (recessionFunction f)

Helper for Corollary 19.5.1: the recession cone of the transformed epigraph of f is the transformed epigraph of recessionFunction f.

theorem helperForCorollary_19_5_1_exists_nonTop_value_of_proper {n : ℕ} {f : (Fin n → ℝ) → EReal} (hproper : ProperConvexFunctionOn Set.univ f) : ∃ (x : Fin n → ℝ), f x ≠ ⊤

Helper for Corollary 19.5.1: a proper convex function takes a non-⊤ value.

theorem helperForCorollary_19_5_1_transformedEpigraph_rightScalarMultiple_polyhedral_of_pos {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfpoly : IsPolyhedralConvexFunction n f) (hproper : ProperConvexFunctionOn Set.univ f) {lam : ℝ} (hlam : 0 < lam) : IsPolyhedralConvexSet (n + 1) ((fun (p : (Fin n → ℝ) × ℝ) => (prodLinearEquiv_append_coord n) p) '' epigraph Set.univ (rightScalarMultiple f lam))

Helper for Corollary 19.5.1: positive right scalar multiples have polyhedral transformed epigraph.

theorem helperForCorollary_19_5_1_zero_scalar_case_polyhedral {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfpoly : IsPolyhedralConvexFunction n f) (hproper : ProperConvexFunctionOn Set.univ f) : IsPolyhedralConvexFunction n (rightScalarMultiple f 0)

Helper for Corollary 19.5.1: the endpoint λ = 0 gives a polyhedral right scalar multiple.

theorem polyhedralConvexFunction_rightScalarMultiple_and_recession (n : ℕ) (f : (Fin n → ℝ) → EReal) : IsPolyhedralConvexFunction n f → ProperConvexFunctionOn Set.univ f → (∀ (lam : ℝ), 0 ≤ lam → IsPolyhedralConvexFunction n (rightScalarMultiple f lam)) ∧ IsPolyhedralConvexFunction n (recessionFunction f)

Corollary 19.5.1: If f is a proper polyhedral convex function, then the right scalar multiple rightScalarMultiple f λ is polyhedral for every λ ≥ 0, and the recession function recessionFunction f (the case λ = 0^+) is polyhedral.

def weightedSumSetWithRecession (n m : ℕ) (C : Fin m → Set (Fin n → ℝ)) (lam : Fin m → ℝ) : Set (Fin n → ℝ)

Weighted sums using λ i • C i for nonzero coefficients and 0^+ C i for zero coefficients.

Equations

• weightedSumSetWithRecession n m C lam = {x : Fin n → ℝ | ∃ (y : Fin m → Fin n → ℝ), (∀ (i : Fin m), y i ∈ if lam i = 0 then (C i).recessionCone else lam i • C i) ∧ x = ∑ i : Fin m, y i}