theorem convexHullFunction_exists_ne_top_of_exists_f_ne_top {n : ℕ} {f : (Fin n → ℝ) → EReal} : (∃ (x : Fin n → ℝ), f x ≠ ⊤) → ∃ (x : Fin n → ℝ), convexHullFunction f x ≠ ⊤

If f is finite somewhere, then so is convexHullFunction f.

theorem posHomGen_convexHullFunction_eq_sInf_pos_rightScalarMultiple {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfinite : ∃ (x : Fin n → ℝ), f x ≠ ⊤) (x : Fin n → ℝ) : x ≠ 0 → positivelyHomogeneousConvexFunctionGenerated (convexHullFunction f) x = sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple (convexHullFunction f) lam x}

Positive-scalar infimum representation for posHomGen of convexHullFunction.

theorem rightScalarMultiple_convexHullFunction_eq_sInf_scaled_convexCombination_add_one {n : ℕ} {f : (Fin n → ℝ) → EReal} (h_not_bot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) {lam : ℝ} (hlam : 0 < lam) (x : Fin n → ℝ) : rightScalarMultiple (convexHullFunction f) lam x = sInf {z : EReal | ∃ (x' : Fin (n + 1) → Fin n → ℝ) (w : Fin (n + 1) → ℝ), IsConvexWeights (n + 1) w ∧ x = ∑ i : Fin (n + 1), (lam * w i) • x' i ∧ z = ∑ i : Fin (n + 1), ↑(lam * w i) * f (x' i)}

Expand rightScalarMultiple of convexHullFunction into scaled convex-combination data.

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

Flatten the positive-scalar infimum into explicit scaled convex-combination data.

theorem scaled_convexCombination_add_one_witness_iff_nonneg_coeff_witness {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hx : x ≠ 0) : sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ ∃ (x' : Fin (n + 1) → Fin n → ℝ) (w : Fin (n + 1) → ℝ), IsConvexWeights (n + 1) w ∧ x = ∑ i : Fin (n + 1), (lam * w i) • x' i ∧ z = ∑ i : Fin (n + 1), ↑(lam * w i) * f (x' i)} = sInf {z : EReal | ∃ (x' : Fin (n + 1) → Fin n → ℝ) (c : Fin (n + 1) → ℝ), (∀ (i : Fin (n + 1)), 0 ≤ c i) ∧ x = ∑ i : Fin (n + 1), c i • x' i ∧ z = ∑ i : Fin (n + 1), ↑(c i) * f (x' i)}

Replace scaled convex weights by nonnegative coefficients (allowing zeros).

theorem toReal_objective_of_sum_ne_top_for_nonnegCoeffs {n m : ℕ} {f : (Fin n → ℝ) → EReal} (h_not_bot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) {x' : Fin m → Fin n → ℝ} {c : Fin m → ℝ} {x : Fin n → ℝ} {z : EReal} (hc : ∀ (i : Fin m), 0 ≤ c i) (hx : x = ∑ i : Fin m, c i • x' i) (hx_ne : x ≠ 0) (hz : z = ∑ i : Fin m, ↑(c i) * f (x' i)) (hz_top : z ≠ ⊤) : ∃ (x'' : Fin m → Fin n → ℝ), x = ∑ i : Fin m, c i • x'' i ∧ (∀ (i : Fin m), f (x'' i) ≠ ⊤) ∧ z = ↑(∑ i : Fin m, c i * (f (x'' i)).toReal)

Convert an EReal objective into a real sum for nonnegative coefficients.

theorem conic_elim_one_generator_pos_obj_to_shorter_fin {n m : ℕ} {x : Fin n → ℝ} (v : Fin (m + 1) → Fin n → ℝ) (c a : Fin (m + 1) → ℝ) (hcpos : ∀ (i : Fin (m + 1)), 0 < c i) (hx : x = ∑ i : Fin (m + 1), c i • v i) (hlin : ¬LinearIndependent ℝ v) (hmin : ∀ (c1 : Fin (m + 1) → ℝ), (∀ (i : Fin (m + 1)), 0 ≤ c1 i) → x = ∑ i : Fin (m + 1), c1 i • v i → ∑ i : Fin (m + 1), c i * a i ≤ ∑ i : Fin (m + 1), c1 i * a i) : ∃ (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

Eliminate one generator from a positive conic combination without increasing a linear objective, assuming the coefficients are objective-minimal among feasible ones.