theorem caratheodory_on_range_preserves_distinct_indices {n k : ℕ} {I : Type u_1} (Cᵢ : I → Set (Fin n → ℝ)) {idx : Fin k → I} {p : Fin k → Fin n → ℝ} {x : Fin n → ℝ} (hidx : Function.Injective idx) (hp : ∀ (j : Fin k), p j ∈ Cᵢ (idx j)) (hx : x ∈ conv (Set.range p)) : ∃ m ≤ n + 1, ∃ (idx' : Fin m → I) (p' : Fin m → Fin n → ℝ) (w : Fin m → ℝ), Function.Injective idx' ∧ (∀ (j : Fin m), p' j ∈ Cᵢ (idx' j)) ∧ AffineIndependent ℝ p' ∧ IsConvexWeights m w ∧ x = convexCombination n m p' w

Apply Carathéodory on a finite range while preserving distinct indices.

theorem mem_conv_iUnion_imp_exists_affineIndependent_convexCombination_le_add_one {n : ℕ} {I : Type u_1} (Cᵢ : I → Set (Fin n → ℝ)) (hconv : ∀ (i : I), Convex ℝ (Cᵢ i)) {x : Fin n → ℝ} : x ∈ conv (⋃ (i : I), Cᵢ i) → ∃ m ≤ n + 1, ∃ (idx : Fin m → I) (p : Fin m → Fin n → ℝ) (w : Fin m → ℝ), Function.Injective idx ∧ (∀ (j : Fin m), p j ∈ Cᵢ (idx j)) ∧ AffineIndependent ℝ p ∧ IsConvexWeights m w ∧ x = convexCombination n m p w

Corollary 17.1.1. Let {Cᵢ | i ∈ I} be an arbitrary collection of convex sets in ℝⁿ, and let C be the convex hull of the union ⋃ i, Cᵢ i. Then every point x ∈ C can be expressed as a convex combination of n + 1 (or fewer) affinely independent points, each belonging to a different Cᵢ.

theorem convexConeGenerated_empty {n : ℕ} : convexConeGenerated n ∅ = {0}

The cone generated by the empty set is just {0}.

theorem mem_convexConeGenerated_imp_exists_nonnegLinearCombination_le {n : ℕ} {T : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hT : T.Nonempty) : x ∈ convexConeGenerated n T → ∃ k ≤ n, ∃ (v : Fin k → Fin n → ℝ) (c : Fin k → ℝ), (∀ (j : Fin k), v j ∈ T) ∧ (∀ (j : Fin k), 0 ≤ c j) ∧ x = ∑ j : Fin k, c j • v j

Extract a bounded nonnegative linear combination from a cone membership.

theorem coalesce_nonnegLinearCombination_iUnion_to_injective {n k : ℕ} {I : Type u_1} (Cᵢ : I → Set (Fin n → ℝ)) (hconv : ∀ (i : I), Convex ℝ (Cᵢ i)) {x : Fin n → ℝ} (v : Fin k → Fin n → ℝ) (c : Fin k → ℝ) (hc : ∀ (j : Fin k), 0 ≤ c j) (hx : x = ∑ j : Fin k, c j • v j) (hmem : ∀ (j : Fin k), ∃ (i : I), v j ∈ Cᵢ i) : ∃ m ≤ k, ∃ (idx : Fin m → I) (v' : Fin m → Fin n → ℝ) (c' : Fin m → ℝ), Function.Injective idx ∧ (∀ (j : Fin m), v' j ∈ Cᵢ (idx j)) ∧ (∀ (j : Fin m), 0 ≤ c' j) ∧ x = ∑ j : Fin m, c' j • v' j

Coalesce a nonnegative linear combination in a union into one indexed by distinct sets.

theorem drop_zero_coeff_sum_smul_to_shorter_fin {n m : ℕ} {y : Fin n → ℝ} (s : Fin (m + 1) → Fin n → ℝ) (c : Fin (m + 1) → ℝ) (hc : ∀ (i : Fin (m + 1)), 0 ≤ c i) (hsum : y = ∑ i : Fin (m + 1), c i • s i) (i0 : Fin (m + 1)) (hci0 : c i0 = 0) : ∃ (e : Fin m ↪ Fin (m + 1)) (c' : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ c' j) ∧ y = ∑ j : Fin m, c' j • s (e j)

Remove a zero coefficient from a nonnegative sum and shorten the index set.

theorem conic_elim_one_generator_pos_to_shorter_fin {n m : ℕ} {y : Fin n → ℝ} (s : Fin (m + 1) → Fin n → ℝ) (c : Fin (m + 1) → ℝ) (hc : ∀ (i : Fin (m + 1)), 0 < c i) (hsum : y = ∑ i : Fin (m + 1), c i • s i) (hlin : ¬LinearIndependent ℝ s) : ∃ (e : Fin m ↪ Fin (m + 1)) (c' : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ c' j) ∧ y = ∑ j : Fin m, c' j • s (e j)

Eliminate one generator from a positive conic combination under linear dependence.

theorem exists_linearIndependent_nonnegLinearCombination_subfamily {n k : ℕ} {x : Fin n → ℝ} (v : Fin k → Fin n → ℝ) (c : Fin k → ℝ) (hc : ∀ (j : Fin k), 0 ≤ c j) (hx : x = ∑ j : Fin k, c j • v j) (hx_ne : x ≠ 0) : ∃ m ≤ k, ∃ (e : Fin m ↪ Fin k) (c' : Fin m → ℝ), (∀ (j : Fin m), 0 ≤ c' j) ∧ (LinearIndependent ℝ fun (j : Fin m) => v (e j)) ∧ x = ∑ j : Fin m, c' j • v (e j)

Reduce a nonnegative sum to a linearly independent subfamily.

theorem mem_convexConeGenerated_iUnion_imp_exists_linearIndependent_nonnegLinearCombination_le {n : ℕ} {I : Type u_1} (Cᵢ : I → Set (Fin n → ℝ)) (hnonempty : ∀ (i : I), (Cᵢ i).Nonempty) (hconv : ∀ (i : I), Convex ℝ (Cᵢ i)) {x : Fin n → ℝ} : x ∈ convexConeGenerated n (⋃ (i : I), Cᵢ i) → x ≠ 0 → ∃ m ≤ n, ∃ (idx : Fin m → I) (v : Fin m → Fin n → ℝ) (c : Fin m → ℝ), Function.Injective idx ∧ (∀ (j : Fin m), v j ∈ Cᵢ (idx j)) ∧ LinearIndependent ℝ v ∧ (∀ (j : Fin m), 0 ≤ c j) ∧ x = ∑ j : Fin m, c j • v j

Corollary 17.1.2. Let {Cᵢ | i ∈ I} be an arbitrary collection of nonempty convex sets in ℝⁿ, and let K be the convex cone generated by the union ⋃ i, Cᵢ i. Then every nonzero vector x ∈ K can be expressed as a nonnegative linear combination of n (or fewer) linearly independent vectors, each belonging to a different Cᵢ.

theorem bdd_toReal_of_sum_ne_top {n : ℕ} {ι : Sort u_1} {f : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) {m : ℕ} {idx : Fin m → ι} {x' : Fin m → Fin n → ℝ} {w : Fin m → ℝ} (hw : IsConvexWeights m w) (hwnz : ∀ (j : Fin m), w j ≠ 0) {z : EReal} (hz : z = ∑ j : Fin m, ↑(w j) * f (idx j) (x' j)) (hz_top : z ≠ ⊤) (j : Fin m) : f (idx j) (x' j) ≠ ⊤

If a convex-weighted EReal sum is not ⊤, then each term is not ⊤.

theorem exists_affine_relation_of_not_affineIndependent {n m : ℕ} {p : Fin (m + 1) → Fin n → ℝ} (h : ¬AffineIndependent ℝ p) : ∃ (μ : Fin (m + 1) → ℝ), ∑ i : Fin (m + 1), μ i = 0 ∧ ∑ i : Fin (m + 1), μ i • p i = 0 ∧ ∃ (i : Fin (m + 1)), μ i ≠ 0

Non-affine-independence yields a nontrivial affine relation.

theorem exists_pos_mu_of_sum_eq_zero_of_ne_zero {m : ℕ} {μ : Fin (m + 1) → ℝ} (hsum : ∑ i : Fin (m + 1), μ i = 0) (hne : ∃ (i : Fin (m + 1)), μ i ≠ 0) : ∃ (i : Fin (m + 1)), 0 < μ i

A nontrivial affine relation with zero sum has a positive coefficient.

theorem convex_elim_one_point_obj_to_shorter_fin {n m : ℕ} {p : Fin (m + 1) → Fin n → ℝ} {w : Fin (m + 1) → ℝ} {x : Fin n → ℝ} {a : Fin (m + 1) → ℝ} (hw : IsConvexWeights (m + 1) w) (hwnz : ∀ (i : Fin (m + 1)), w i ≠ 0) (hx : x = convexCombination n (m + 1) p w) (hdep : ¬AffineIndependent ℝ p) : ∃ (i0 : Fin (m + 1)) (w1 : Fin (m + 1) → ℝ), IsConvexWeights (m + 1) w1 ∧ x = convexCombination n (m + 1) p w1 ∧ w1 i0 = 0 ∧ ∑ i : Fin (m + 1), w1 i * a i ≤ ∑ i : Fin (m + 1), w i * a i

Eliminate one point from a convex combination while not increasing a linear objective.