theorem rightScalarMultiple_convexHullFamily_eq_sInf_scaled_affineIndependent {n : ℕ} {ι : Type u_1} {fᵢ : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (fᵢ i)) {lam : ℝ} (hlam : 0 < lam) (x : Fin n → ℝ) : rightScalarMultiple (convexHullFunctionFamily fᵢ) lam x = sInf {z : EReal | ∃ m ≤ n + 1, ∃ (idx : Fin m → ι) (p : Fin m → Fin n → ℝ) (w : Fin m → ℝ), IsConvexWeights m w ∧ (∀ (j : Fin m), w j ≠ 0) ∧ x = ∑ j : Fin m, (lam * w j) • p j ∧ AffineIndependent ℝ p ∧ z = ∑ j : Fin m, ↑(lam * w j) * fᵢ (idx j) (p j)}

Expand rightScalarMultiple of a convex-hull family into scaled convex-combination data.

theorem iInf_sInf_eq_sInf_exists {α : Sort u_1} (B : α → Set EReal) : ⨅ (a : α), sInf (B a) = sInf {z : EReal | ∃ (a : α), z ∈ B a}

Flatten an iInf of sInf into a single sInf over existentials.

theorem sInf_pos_rightScalarMultiple_eq_sInf_exists_scaled_convexCombo {n : ℕ} {ι : Type u_1} {fᵢ : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (fᵢ i)) (x : Fin n → ℝ) : sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple (convexHullFunctionFamily fᵢ) lam x} = sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ ∃ m ≤ n + 1, ∃ (idx : Fin m → ι) (p : Fin m → Fin n → ℝ) (w : Fin m → ℝ), IsConvexWeights m w ∧ (∀ (j : Fin m), w j ≠ 0) ∧ x = ∑ j : Fin m, (lam * w j) • p j ∧ AffineIndependent ℝ p ∧ z = ∑ j : Fin m, ↑(lam * w j) * fᵢ (idx j) (p j)}

Reparameterize the infimum over positive right scalar multiples into explicit data.

theorem scaled_convexCombo_witness_iff_pos_coeff_witness {n : ℕ} {ι : Type u_1} {fᵢ : ι → (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hx : x ≠ 0) : sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ ∃ m ≤ n + 1, ∃ (idx : Fin m → ι) (p : Fin m → Fin n → ℝ) (w : Fin m → ℝ), IsConvexWeights m w ∧ (∀ (j : Fin m), w j ≠ 0) ∧ x = ∑ j : Fin m, (lam * w j) • p j ∧ AffineIndependent ℝ p ∧ z = ∑ j : Fin m, ↑(lam * w j) * fᵢ (idx j) (p j)} = sInf {z : EReal | ∃ m ≤ n + 1, ∃ (idx : Fin m → ι) (p : Fin m → Fin n → ℝ) (c : Fin m → ℝ), (∀ (j : Fin m), 0 < c j) ∧ x = ∑ j : Fin m, c j • p j ∧ AffineIndependent ℝ p ∧ z = ∑ j : Fin m, ↑(c j) * fᵢ (idx j) (p j)}

Replace scaled convex weights by strictly positive coefficients.

theorem drop_zero_coeff_sum_smul_and_sum_mul_to_shorter_fin {n m : ℕ} {x : Fin n → ℝ} (v : Fin (m + 1) → Fin n → ℝ) (c a : Fin (m + 1) → ℝ) (hc : ∀ (i : Fin (m + 1)), 0 ≤ c i) (hx : x = ∑ i : Fin (m + 1), c i • v i) (i0 : Fin (m + 1)) (hci0 : c i0 = 0) : ∃ (e : Fin m ↪ Fin (m + 1)) (c' : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ c' j) ∧ x = ∑ j : Fin m, c' j • v (e j) ∧ ∑ j : Fin m, c' j * a (e j) = ∑ i : Fin (m + 1), c i * a i

Drop a zero coefficient in a conic sum while preserving the linear objective.

theorem positivelyHomogeneousConvexFunctionGenerated_convexHullFunctionFamily_eq_sInf_linearIndependent_nonnegLinearCombination_le {n : ℕ} {ι : Type u_1} {fᵢ : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (fᵢ i)) (x : Fin n → ℝ) : x ≠ 0 → positivelyHomogeneousConvexFunctionGenerated (convexHullFunctionFamily fᵢ) x = sInf {z : EReal | ∃ m ≤ n + 1, ∃ (idx : Fin m → ι) (x' : Fin m → Fin n → ℝ) (c : Fin m → ℝ), (∀ (j : Fin m), 0 < c j) ∧ x = ∑ j : Fin m, c j • x' j ∧ AffineIndependent ℝ x' ∧ z = ∑ j : Fin m, ↑(c j) * fᵢ (idx j) (x' j)}

Corollary 17.1.4. Let {fᵢ | i ∈ I} be an arbitrary collection of proper convex functions on ℝⁿ. Let f be the greatest positively homogeneous convex function such that f ≤ fᵢ i for every i, i.e. the positively homogeneous convex function generated by conv {fᵢ | i ∈ I}.

Then, for every vector x ≠ 0, one has

f x = inf { ∑ j, λ j * fᵢ (idx j) (xⱼ j) | x = ∑ j, λ j • xⱼ j },

where the infimum is taken over all expressions of x as a positive linear combination of at most n + 1 vectors, which are affinely independent.

theorem pad_convexCombination_succ {n m : ℕ} {x' : Fin m → Fin n → ℝ} {w : Fin m → ℝ} (hw : IsConvexWeights m w) (x0 : Fin n → ℝ) : IsConvexWeights (m + 1) (Fin.cons 0 w) ∧ convexCombination n (m + 1) (Fin.cons x0 x') (Fin.cons 0 w) = convexCombination n m x' w

Pad a convex combination by one zero-weight entry.

theorem pad_objective_sum_succ {n m : ℕ} {f : (Fin n → ℝ) → EReal} {x0 : Fin n → ℝ} {x' : Fin m → Fin n → ℝ} {w : Fin m → ℝ} : ∑ i : Fin (m + 1), ↑(Fin.cons 0 w i) * f (Fin.cons x0 x' i) = ∑ i : Fin m, ↑(w i) * f (x' i)

Padding by a zero weight leaves the objective sum unchanged.

theorem pad_convexCombination_to_fin_add_one {n m : ℕ} {f : (Fin n → ℝ) → EReal} (hm : m ≤ n + 1) {x' : Fin m → Fin n → ℝ} {w : Fin m → ℝ} (hw : IsConvexWeights m w) : ∃ (x'' : Fin (n + 1) → Fin n → ℝ) (w'' : Fin (n + 1) → ℝ), IsConvexWeights (n + 1) w'' ∧ convexCombination n (n + 1) x'' w'' = convexCombination n m x' w ∧ ∑ i : Fin (n + 1), ↑(w'' i) * f (x'' i) = ∑ i : Fin m, ↑(w i) * f (x' i)

Pad a convex combination to length n + 1, preserving the weighted sum.

theorem toReal_objective_of_sum_ne_top_for_weights {n m : ℕ} {f : (Fin n → ℝ) → EReal} (h_not_bot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) {x' : Fin m → Fin n → ℝ} {w : Fin m → ℝ} {x : Fin n → ℝ} {z : EReal} (hw : IsConvexWeights m w) (hx : x = convexCombination n m x' w) (hz : z = ∑ i : Fin m, ↑(w i) * f (x' i)) (hz_top : z ≠ ⊤) : ∃ (x'' : Fin m → Fin n → ℝ), x = convexCombination n m x'' w ∧ (∀ (i : Fin m), f (x'' i) ≠ ⊤) ∧ z = ↑(∑ i : Fin m, w i * (f (x'' i)).toReal)

Convert an EReal objective into a real sum when the total is not ⊤.

theorem reduce_convexCombo_objective_to_le_add_one {n k : ℕ} {p : Fin k → Fin n → ℝ} {w : Fin k → ℝ} {x : Fin n → ℝ} {a : Fin k → ℝ} (hw : IsConvexWeights k w) (hx : x = convexCombination n k p w) : ∃ m ≤ n + 1, ∃ (e : Fin m ↪ Fin k) (w' : Fin m → ℝ), IsConvexWeights m w' ∧ x = convexCombination n m (fun (j : Fin m) => p (e j)) w' ∧ ∑ j : Fin m, w' j * a (e j) ≤ ∑ i : Fin k, w i * a i

Reduce a convex-combination objective to at most n + 1 points.

theorem convexHullFunction_eq_sInf_convexCombination_add_one {n : ℕ} {f : (Fin n → ℝ) → EReal} (h_not_bot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (x : Fin n → ℝ) : convexHullFunction f x = sInf {z : EReal | ∃ (x' : Fin (n + 1) → Fin n → ℝ) (w : Fin (n + 1) → ℝ), IsConvexWeights (n + 1) w ∧ x = convexCombination n (n + 1) x' w ∧ z = ∑ i : Fin (n + 1), ↑(w i) * f (x' i)}

Corollary 17.1.5. Let f : ℝⁿ → (-∞, +∞] be any function (modeled here as f : (Fin n → ℝ) → EReal together with the side condition ∀ x, f x ≠ ⊥). Then [ (\text{conv } f)(x) = \inf \Bigl{ \sum_{i=1}^{n+1} \lambda_i f(x_i) ,\Bigm|, \sum_{i=1}^{n+1} \lambda_i x_i = x \Bigr}, ] where the infimum is taken over all expressions of x as a convex combination of n + 1 points. (The same formula holds if one restricts to convex combinations in which the n + 1 points are affinely independent.)