theorem drop_zero_weights_preserves_convexCombination_obj {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) (hzero : ∃ (i : Fin k), w i = 0) : ∃ (k' : ℕ) (e : Fin k' ↪ Fin k) (w' : Fin k' → ℝ), IsConvexWeights k' w' ∧ (∀ (j : Fin k'), w' j ≠ 0) ∧ x = convexCombination n k' (fun (j : Fin k') => p (e j)) w' ∧ ∑ j : Fin k', w' j * a (e j) = ∑ i : Fin k, w i * a i ∧ k' < k

Remove zero weights from a convex combination while preserving the point and objective.

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

Reduce a convex combination to an affinely independent one without increasing a linear objective.

theorem B0_mem_to_Fin_pos_repr {n : ℕ} {ι : Type u_1} {f : ι → (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {z : EReal} {s : Finset ι} {lam : ι → ℝ} {x' : ι → Fin n → ℝ} (h0 : ∀ (i : ι), 0 ≤ lam i) (hsum1 : ∑ i ∈ s, lam i = 1) (hsumx : ∑ i ∈ s, lam i • x' i = x) (hz : z = ∑ i ∈ s, ↑(lam i) * f i (x' i)) : ∃ (k : ℕ) (idx : Fin k → ι) (p : Fin k → Fin n → ℝ) (w : Fin k → ℝ), IsConvexWeights k w ∧ (∀ (j : Fin k), w j ≠ 0) ∧ x = convexCombination n k p w ∧ z = ∑ j : Fin k, ↑(w j) * f (idx j) (p j)

Reindex a finset convex-combination witness to Fin k with nonzero weights.

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

theorem convexHullFunctionFamily_convex_and_exists_ne_top {n : ℕ} {ι : Sort u_1} {fᵢ : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (fᵢ i)) (hI : Nonempty ι) : ConvexFunctionOn Set.univ (convexHullFunctionFamily fᵢ) ∧ ∃ (x : Fin n → ℝ), convexHullFunctionFamily fᵢ x ≠ ⊤

Convexity and a finite point for convexHullFunctionFamily under properness.

theorem posHomGen_convexHullFamily_eq_sInf_pos_rightScalarMultiple {n : ℕ} {ι : Sort u_1} {fᵢ : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (fᵢ i)) (hI : Nonempty ι) (x : Fin n → ℝ) : x ≠ 0 → positivelyHomogeneousConvexFunctionGenerated (convexHullFunctionFamily fᵢ) x = sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple (convexHullFunctionFamily fᵢ) lam x}

Positive-scalar infimum representation for posHomGen of a convex hull family.

theorem convexHullFunctionFamily_eq_top_of_isEmpty {n : ℕ} {ι : Type u_1} {fᵢ : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (fᵢ i)) (hI : IsEmpty ι) (x : Fin n → ℝ) : convexHullFunctionFamily fᵢ x = ⊤

If the index type is empty, the convex hull family is identically ⊤.

theorem posHomGen_convexHullFamily_eq_top_of_isEmpty {n : ℕ} {ι : Type u_1} {fᵢ : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (fᵢ i)) (hI : IsEmpty ι) (x : Fin n → ℝ) : x ≠ 0 → positivelyHomogeneousConvexFunctionGenerated (convexHullFunctionFamily fᵢ) x = ⊤

In the empty-index case, the generated positively homogeneous convex function is ⊤ off zero.

theorem cor17_1_4_rhs_empty_of_isEmpty {n : ℕ} {ι : Sort u_1} {fᵢ : ι → (Fin n → ℝ) → EReal} (hI : IsEmpty ι) {x : Fin n → ℝ} (hx : x ≠ 0) : {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)} = ∅

In the empty-index case, the witness set for Corollary 17.1.4 is empty off zero.

noncomputable def ereal_mulPosOrderIso (t : ℝ) (ht : 0 < t) : EReal ≃o EReal

Multiplication by a positive real number is an order isomorphism on EReal.

Equations

• ereal_mulPosOrderIso t ht = { toFun := fun (x : EReal) => ↑t * x, invFun := fun (x : EReal) => ↑t⁻¹ * x, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem ereal_mul_sum {ι : Type u_1} (s : Finset ι) (f : ι → EReal) (a : EReal) (ha_nonneg : 0 ≤ a) (ha_ne_top : a ≠ ⊤) : a * s.sum f = ∑ i ∈ s, a * f i

Left multiplication by a nonnegative, non-top EReal distributes over finite sums.