Convex Analysis (Rockafellar, 1970) -- Chapter 04 -- Section 17 -- Part 4
open scoped BigOperators Pointwiseopen Topologysection Chap04section Section17Apply Carathéodory on a finite range while preserving distinct indices.
lemma caratheodory_on_range_preserves_distinct_indices
{n k : Nat} {I : Type*} (Cᵢ : I → Set (Fin n → Real))
{idx : Fin k → I} {p : Fin k → Fin n → Real} {x : Fin n → Real}
(hidx : Function.Injective idx) (hp : ∀ j, p j ∈ Cᵢ (idx j))
(hx : x ∈ conv (Set.range p)) :
∃ m : Nat, m ≤ n + 1 ∧
∃ (idx' : Fin m → I) (p' : Fin m → Fin n → Real) (w : Fin m → Real),
Function.Injective idx' ∧ (∀ j, p' j ∈ Cᵢ (idx' j)) ∧
AffineIndependent ℝ p' ∧ IsConvexWeights m w ∧ x = convexCombination n m p' w := by
classical
obtain ⟨ι, _inst, z, w, hz_range, hz_aff, hw_pos, hw_sum, hw_x⟩ :=
caratheodory_aux_exists_affineIndependent_pos (n := n) (S := Set.range p) (x := x) hx
have hm_le : Fintype.card ι ≤ n + 1 :=
caratheodory_aux_card_le_n_add_one (n := n) (z := z) hz_aff
have hchoice : ∀ i, ∃ j, z i = p j := by
intro i
rcases hz_range ⟨i, rfl⟩ with ⟨j, hj⟩
exact ⟨j, hj.symm⟩
choose jOf hjOf using hchoice
let idx0 : ι → I := fun i => idx (jOf i)
have hidx0 : Function.Injective idx0 := by
intro i1 i2 h
have hj : jOf i1 = jOf i2 := hidx (by simpa [idx0] using h)
have hz_inj : Function.Injective z := hz_aff.injective
apply hz_inj
calc
z i1 = p (jOf i1) := hjOf i1
_ = p (jOf i2) := by simp [hj]
_ = z i2 := (hjOf i2).symm
let m : Nat := Fintype.card ι
let e : ι ≃ Fin m := Fintype.equivFin ι
let p' : Fin m → Fin n → Real := fun j => z (e.symm j)
let w' : Fin m → Real := fun j => w (e.symm j)
let idx' : Fin m → I := fun j => idx0 (e.symm j)
have hidx' : Function.Injective idx' := by
intro j1 j2 h
have h' : idx0 (e.symm j1) = idx0 (e.symm j2) := by
simpa [idx'] using h
have h'' : e.symm j1 = e.symm j2 := hidx0 h'
exact e.symm.injective h''
have hp' : ∀ j, p' j ∈ Cᵢ (idx' j) := by
intro j
have : p (jOf (e.symm j)) ∈ Cᵢ (idx (jOf (e.symm j))) := hp (jOf (e.symm j))
simpa [p', idx', idx0, hjOf] using this
have h_aff' : AffineIndependent ℝ p' := by
simpa [p'] using (AffineIndependent.comp_embedding (f := e.symm.toEmbedding) hz_aff)
have hw' : IsConvexWeights m w' := by
refine ⟨?_, ?_⟩
· intro j
exact le_of_lt (hw_pos (e.symm j))
· have hsum' : (∑ j, w' j) = ∑ i, w i := by
simpa [w'] using (Equiv.sum_comp e.symm (fun i => w i))
calc
∑ j, w' j = ∑ i, w i := hsum'
_ = 1 := hw_sum
have hx_eq : x = convexCombination n m p' w' := by
have hsum' : (∑ j, w' j • p' j) = ∑ i, w i • z i := by
simpa [w', p'] using (Equiv.sum_comp e.symm (fun i => w i • z i))
calc
x = ∑ i, w i • z i := by
simpa using hw_x.symm
_ = ∑ j, w' j • p' j := by
symm
exact hsum'
_ = convexCombination n m p' w' := by
simp [convexCombination]
refine ⟨m, ?_, idx', p', w', hidx', hp', h_aff', hw', hx_eq⟩
simpa [m] using hm_le
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 mem_conv_iUnion_imp_exists_affineIndependent_convexCombination_le_add_one
{n : Nat} {I : Type*} (Cᵢ : I → Set (Fin n → Real)) (hconv : ∀ i, Convex ℝ (Cᵢ i))
{x : Fin n → Real} :
x ∈ conv (⋃ i, Cᵢ i) →
∃ m : Nat, m ≤ n + 1 ∧
∃ (idx : Fin m → I) (p : Fin m → Fin n → Real) (w : Fin m → Real),
Function.Injective idx ∧ (∀ j, p j ∈ Cᵢ (idx j)) ∧
AffineIndependent ℝ p ∧ IsConvexWeights m w ∧ x = convexCombination n m p w := by
intro hx
obtain ⟨k, idx, p, w, hidx, hp, hw, hx_eq⟩ :=
exists_injective_indexed_convexCombination_of_mem_conv_iUnion
(Cᵢ := Cᵢ) (hconv := hconv) (x := x) hx
have hx_range : x ∈ conv (Set.range p) :=
conv_mem_range_of_convexCombination (p := p) (w := w) (x := x) hw hx_eq
rcases
caratheodory_on_range_preserves_distinct_indices
(Cᵢ := Cᵢ) (idx := idx) (p := p) (x := x) hidx hp hx_range with
⟨m, hm, idx', p', w', hidx', hp', haff, hw', hx'⟩
exact ⟨m, hm, idx', p', w', hidx', hp', haff, hw', hx'⟩
The cone generated by the empty set is just {0}.
lemma convexConeGenerated_empty {n : Nat} :
convexConeGenerated n (∅ : Set (Fin n → Real)) = ({0} : Set (Fin n → Real)) := by
classical
have hle :
ConvexCone.hull Real (∅ : Set (Fin n → Real)) ≤
(⊥ : ConvexCone Real (Fin n → Real)) := by
refine ConvexCone.hull_min ?_
intro x hx
cases hx
have hge :
(⊥ : ConvexCone Real (Fin n → Real)) ≤
ConvexCone.hull Real (∅ : Set (Fin n → Real)) := by
exact bot_le
have hhull :
ConvexCone.hull Real (∅ : Set (Fin n → Real)) =
(⊥ : ConvexCone Real (Fin n → Real)) :=
le_antisymm hle hge
ext x
constructor
· intro hx
have hx' :
x = 0 ∨ x ∈ (ConvexCone.hull Real (∅ : Set (Fin n → Real)) : Set (Fin n → Real)) := by
simpa [convexConeGenerated] using hx
cases hx' with
| inl h =>
simp [h]
| inr h =>
have : False := by
simp [hhull] at h
exact this.elim
· intro hx
rcases (Set.mem_singleton_iff.mp hx) with rfl
exact (Set.mem_insert_iff).2 (Or.inl rfl)Extract a bounded nonnegative linear combination from a cone membership.
lemma mem_convexConeGenerated_imp_exists_nonnegLinearCombination_le
{n : Nat} {T : Set (Fin n → Real)} {x : Fin n → Real} (hT : T.Nonempty) :
x ∈ convexConeGenerated n T →
∃ k : Nat, k ≤ n ∧
∃ v : Fin k → Fin n → Real, ∃ c : Fin k → Real,
(∀ j, v j ∈ T) ∧ (∀ j, 0 ≤ c j) ∧ x = ∑ j, c j • v j := by
intro hx
have hx' :
x ∈ mixedConvexHull ({0} : Set (Fin n → Real)) T := by
simpa [convexConeGenerated_eq_mixedConvexHull_singleton_zero] using hx
rcases
(mem_mixedConvexHull_iff_exists_mixedConvexCombination_le_finrank_add_one
(n := n) ({0} : Set (Fin n → Real)) T x).1 hx' with
⟨m, hm, hcomb⟩
rcases
isMixedConvexCombination_singleton_zero_imp_exists_nonnegLinearCombination
(n := n) (m := m) (T := T) (x := x) hT hcomb with
⟨y, c, hy, hc, hsum⟩
refine ⟨m - 1, ?_, y, c, hy, hc, hsum⟩
exact (Nat.sub_le_iff_le_add).2 (by simpa using hm)Coalesce a nonnegative linear combination in a union into one indexed by distinct sets.
lemma coalesce_nonnegLinearCombination_iUnion_to_injective
{n k : Nat} {I : Type*} (Cᵢ : I → Set (Fin n → Real)) (hconv : ∀ i, Convex ℝ (Cᵢ i))
{x : Fin n → Real} (v : Fin k → Fin n → Real) (c : Fin k → Real)
(hc : ∀ j, 0 ≤ c j) (hx : x = ∑ j, c j • v j)
(hmem : ∀ j, ∃ i, v j ∈ Cᵢ i) :
∃ m : Nat, m ≤ k ∧
∃ (idx : Fin m → I) (v' : Fin m → Fin n → Real) (c' : Fin m → Real),
Function.Injective idx ∧ (∀ j, v' j ∈ Cᵢ (idx j)) ∧
(∀ j, 0 ≤ c' j) ∧ x = ∑ j, c' j • v' j := by
classical
choose idx0 hidx0_mem using hmem
let s : Finset I := Finset.image idx0 Finset.univ
let μ : I → Real := fun b =>
∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i
let t : Finset I := s.filter (fun b => μ b ≠ 0)
let y : I → Fin n → Real := fun b =>
if h : μ b = 0 then 0
else (1 / μ b) • ∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i • v i
have hμ_nonneg : ∀ b, 0 ≤ μ b := by
intro b
refine Finset.sum_nonneg ?_
intro i hi
exact hc i
have hy_mem : ∀ b ∈ t, y b ∈ Cᵢ b := by
intro b hb
have hμ : μ b ≠ 0 := (Finset.mem_filter.1 hb).2
have hμ_pos : 0 < μ b := lt_of_le_of_ne (hμ_nonneg b) (Ne.symm hμ)
let fiber : Finset (Fin k) := Finset.univ.filter (fun i => idx0 i = b)
have hweights_nonneg : ∀ i ∈ fiber, 0 ≤ c i / μ b := by
intro i hi
exact div_nonneg (hc i) (le_of_lt hμ_pos)
have hweights_sum : ∑ i ∈ fiber, c i / μ b = (1 : Real) := by
have hμ_ne : μ b ≠ 0 := hμ
calc
∑ i ∈ fiber, c i / μ b
= ∑ i ∈ fiber, c i * (μ b)⁻¹ := by
simp [div_eq_mul_inv]
_ = (∑ i ∈ fiber, c i) * (μ b)⁻¹ := by
simpa using
(Finset.sum_mul (s := fiber) (f := c) (a := (μ b)⁻¹)).symm
_ = μ b * (μ b)⁻¹ := by
simp [μ, fiber]
_ = 1 := by
simp [hμ_ne]
have hz_mem' : ∀ i ∈ fiber, v i ∈ Cᵢ b := by
intro i hi
have hidx : idx0 i = b := (Finset.mem_filter.1 hi).2
simpa [hidx] using hidx0_mem i
have hy' :
(∑ i ∈ fiber, (c i / μ b) • v i) ∈ Cᵢ b :=
(hconv b).sum_mem hweights_nonneg hweights_sum hz_mem'
have hy_eq :
y b = ∑ i ∈ fiber, (c i / μ b) • v i := by
have hμ_ne : μ b ≠ 0 := hμ
calc
y b = (1 / μ b) • ∑ i ∈ fiber, c i • v i := by
simp [y, hμ, fiber]
_ = ∑ i ∈ fiber, (1 / μ b) • (c i • v i) := by
simpa using (Finset.smul_sum (s := fiber) (f := fun i => c i • v i) (r := 1 / μ b))
_ = ∑ i ∈ fiber, (c i / μ b) • v i := by
refine Finset.sum_congr rfl ?_
intro i hi
simp [div_eq_mul_inv, smul_smul, mul_comm]
simpa [hy_eq] using hy'
have hy_mul :
∀ b ∈ s, μ b • y b =
∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i • v i := by
intro b hb
by_cases hμ : μ b = 0
· have hsum_weights :
∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i = 0 := by
simp [μ, hμ]
have hzero :
∀ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i = 0 := by
have hnonneg :
∀ i ∈ Finset.univ.filter (fun i => idx0 i = b), 0 ≤ c i := by
intro i hi
exact hc i
exact (Finset.sum_eq_zero_iff_of_nonneg hnonneg).1 hsum_weights
have hsum_zero :
∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i • v i = 0 := by
refine Finset.sum_eq_zero ?_
intro i hi
simp [hzero i hi]
simp [y, hμ, hsum_zero]
· have hμ_ne : μ b ≠ 0 := hμ
have hsum :
μ b • y b =
μ b • ((1 / μ b) •
∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i • v i) := by
simp [y, hμ]
calc
μ b • y b =
μ b • ((1 / μ b) •
∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i • v i) := hsum
_ = (μ b * (1 / μ b)) •
∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i • v i := by
simp [smul_smul]
_ = ∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i • v i := by
simp [div_eq_mul_inv, hμ_ne]
have hsum_y : ∑ b ∈ s, μ b • y b = ∑ i, c i • v i := by
have hmaps :
∀ i ∈ (Finset.univ : Finset (Fin k)), idx0 i ∈ s := by
intro i hi
exact Finset.mem_image_of_mem idx0 (Finset.mem_univ i)
calc
∑ b ∈ s, μ b • y b =
∑ b ∈ s, ∑ i ∈ Finset.univ.filter (fun i => idx0 i = b), c i • v i := by
refine Finset.sum_congr rfl ?_
intro b hb
simp [hy_mul b hb]
_ = ∑ i ∈ (Finset.univ : Finset (Fin k)), c i • v i := by
simpa using
(Finset.sum_fiberwise_of_maps_to (s := (Finset.univ : Finset (Fin k))) (t := s)
(g := idx0) (f := fun i => c i • v i) hmaps)
_ = ∑ i, c i • v i := by simp
have hx_sum : x = ∑ b ∈ s, μ b • y b := by
calc
x = ∑ i, c i • v i := hx
_ = ∑ b ∈ s, μ b • y b := by
symm
exact hsum_y
have hx_sum_t : x = ∑ b ∈ t, μ b • y b := by
have hsum_t_eq :
∑ b ∈ t, μ b • y b = ∑ b ∈ s, μ b • y b := by
have hsum' :
∑ b ∈ s.filter (fun b => μ b ≠ 0), μ b • y b = ∑ b ∈ s, μ b • y b := by
refine (Finset.sum_filter_of_ne (s := s) (p := fun b => μ b ≠ 0)
(f := fun b => μ b • y b) ?_)
intro b hb hne
by_contra hμ
apply hne
simp [hμ]
simpa [t] using hsum'
calc
x = ∑ b ∈ s, μ b • y b := hx_sum
_ = ∑ b ∈ t, μ b • y b := by
symm
exact hsum_t_eq
let m : Nat := t.card
let e : t ≃ Fin m := t.equivFin
let idx : Fin m → I := fun j => (e.symm j).1
let v' : Fin m → Fin n → Real := fun j => y (e.symm j).1
let c' : Fin m → Real := fun j => μ (e.symm j).1
have hidx : Function.Injective idx := by
intro j1 j2 h
apply e.symm.injective
apply Subtype.ext
simpa [idx] using h
have hv' : ∀ j, v' j ∈ Cᵢ (idx j) := by
intro j
have hb : (e.symm j).1 ∈ t := (e.symm j).2
exact hy_mem _ hb
have hc' : ∀ j, 0 ≤ c' j := by
intro j
exact hμ_nonneg _
have hx_eq : x = ∑ j, c' j • v' j := by
have hx_subtype : x = ∑ b : t, μ b.1 • y b.1 := by
have hsum_subtype :
∑ b ∈ t, μ b • y b = ∑ b : t, μ b.1 • y b.1 := by
refine Finset.sum_subtype (s := t) (p := fun b => b ∈ t)
(f := fun b => μ b • y b) ?_
intro b
simp
calc
x = ∑ b ∈ t, μ b • y b := hx_sum_t
_ = ∑ b : t, μ b.1 • y b.1 := hsum_subtype
have hsum_fin :
∑ j, c' j • v' j = ∑ b : t, μ b.1 • y b.1 := by
simpa [c', v'] using (Equiv.sum_comp e.symm (fun b : t => μ b.1 • y b.1))
calc
x = ∑ b : t, μ b.1 • y b.1 := hx_subtype
_ = ∑ j, c' j • v' j := by
symm
exact hsum_fin
have hm_le : m ≤ k := by
have hs_le : s.card ≤ k := by
simpa [s] using
(Finset.card_image_le (s := (Finset.univ : Finset (Fin k))) (f := idx0))
have ht_le : t.card ≤ s.card := by
simpa [t] using (Finset.card_filter_le (s := s) (p := fun b => μ b ≠ 0))
exact le_trans ht_le hs_le
exact ⟨m, hm_le, idx, v', c', hidx, hv', hc', hx_eq⟩Remove a zero coefficient from a nonnegative sum and shorten the index set.
lemma drop_zero_coeff_sum_smul_to_shorter_fin {n m : Nat}
{y : Fin n → Real}
(s : Fin (m + 1) → Fin n → Real) (c : Fin (m + 1) → Real)
(hc : ∀ i, 0 ≤ c i) (hsum : y = ∑ i, c i • s i)
(i0 : Fin (m + 1)) (hci0 : c i0 = 0) :
∃ e : Fin m ↪ Fin (m + 1), ∃ c' : Fin m → Real,
(∀ j, 0 ≤ c' j) ∧ y = ∑ j, c' j • s (e j) := by
classical
let I : Type := {i : Fin (m + 1) // i ≠ i0}
let e' : Fin m ≃ I := finSuccAboveEquiv i0
let e : Fin m ↪ Fin (m + 1) :=
{ toFun := fun j => (e' j).1
inj' := by
intro j1 j2 h
have h' : e' j1 = e' j2 := by
apply Subtype.ext
simpa using h
exact e'.injective h' }
let c' : Fin m → Real := fun j => c (e j)
have hc' : ∀ j, 0 ≤ c' j := by
intro j
simpa [c', e] using hc (e' j).1
have hsum_filter :
(∑ i, c i • s i) =
∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c i • s i := by
have hsum_if :
(∑ i, c i • s i) = ∑ i, (if i ≠ i0 then c i • s i else 0) := by
refine Finset.sum_congr rfl ?_
intro i _hi
by_cases h : i = i0
· subst h
simp [hci0]
· simp [h]
have hsum_filter' :
∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c i • s i =
∑ i, (if i ≠ i0 then c i • s i else 0) := by
simpa using
(Finset.sum_filter (s := (Finset.univ : Finset (Fin (m + 1))))
(f := fun i => c i • s i) (p := fun i => i ≠ i0))
calc
(∑ i, c i • s i) = ∑ i, (if i ≠ i0 then c i • s i else 0) := hsum_if
_ = ∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c i • s i := by
symm
exact hsum_filter'
have hsum_subtype :
∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c i • s i =
∑ i : I, c i.1 • s i.1 := by
refine (Finset.sum_subtype (s := Finset.univ.filter (fun i => i ≠ i0))
(p := fun i => i ≠ i0) (f := fun i => c i • s i) ?_)
intro i
simp
have hsum_I : y = ∑ i : I, c i.1 • s i.1 := by
calc
y = ∑ i, c i • s i := hsum
_ = ∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c i • s i := hsum_filter
_ = ∑ i : I, c i.1 • s i.1 := hsum_subtype
have hsum_equiv :
∑ j, c' j • s (e j) = ∑ i : I, c i.1 • s i.1 := by
simpa [c', e] using
(Equiv.sum_comp e' (fun i : I => c i.1 • s i.1))
refine ⟨e, c', hc', ?_⟩
calc
y = ∑ i : I, c i.1 • s i.1 := hsum_I
_ = ∑ j, c' j • s (e j) := by
symm
exact hsum_equivEliminate one generator from a positive conic combination under linear dependence.
lemma conic_elim_one_generator_pos_to_shorter_fin {n m : Nat}
{y : Fin n → Real}
(s : Fin (m + 1) → Fin n → Real) (c : Fin (m + 1) → Real)
(hc : ∀ i, 0 < c i) (hsum : y = ∑ i, c i • s i)
(hlin : ¬ LinearIndependent ℝ s) :
∃ e : Fin m ↪ Fin (m + 1), ∃ c' : Fin m → Real,
(∀ j, 0 ≤ c' j) ∧ y = ∑ j, c' j • s (e j) := by
classical
obtain ⟨μ, hμsum, hμpos⟩ :=
exists_linear_relation_sum_smul_eq_zero_exists_pos (s := s) hlin
let P : Finset (Fin (m + 1)) := Finset.univ.filter (fun i => 0 < μ i)
have hPne : P.Nonempty := by
rcases hμpos with ⟨i, hi⟩
refine ⟨i, ?_⟩
simp [P, hi]
obtain ⟨i0, hi0P, hmin⟩ := Finset.exists_min_image P (fun i => c i / μ i) hPne
have hμi0 : 0 < μ i0 := (Finset.mem_filter.mp hi0P).2
have hμi0_ne : μ i0 ≠ 0 := ne_of_gt hμi0
let lam : Real := c i0 / μ i0
let c1 : Fin (m + 1) → Real := fun i => c i - lam * μ i
have hlamnonneg : 0 ≤ lam := by
exact div_nonneg (le_of_lt (hc i0)) (le_of_lt hμi0)
have hci0 : c1 i0 = 0 := by
have hmul : (c i0 / μ i0) * μ i0 = c i0 := by
field_simp [hμi0_ne]
have hmul' : lam * μ i0 = c i0 := by
simpa [lam] using hmul
simp [c1, hmul']
have hc1 : ∀ i, 0 ≤ c1 i := by
intro i
by_cases hμpos_i : 0 < μ i
· have hi : i ∈ P := by
simp [P, hμpos_i]
have hmin_i : lam ≤ c i / μ i := hmin i hi
have hle : lam * μ i ≤ c i := (le_div_iff₀ hμpos_i).1 hmin_i
exact sub_nonneg_of_le hle
· have hμle : μ i ≤ 0 := le_of_not_gt hμpos_i
have hterm : 0 ≤ -lam * μ i := by
have : 0 ≤ lam * (-μ i) := mul_nonneg hlamnonneg (neg_nonneg.mpr hμle)
simpa [mul_comm, mul_left_comm, mul_assoc, mul_neg, neg_mul] using this
have hc_nonneg : 0 ≤ c i := le_of_lt (hc i)
have : 0 ≤ c i + (-lam * μ i) := add_nonneg hc_nonneg hterm
simpa [c1, sub_eq_add_neg, add_comm, add_left_comm, add_assoc,
mul_comm, mul_left_comm, mul_assoc] using this
have hsum_c1 : y = ∑ i, c1 i • s i := by
have hsum_expand :
∑ i, c i • s i = ∑ i, c1 i • s i + lam • ∑ i, μ i • s i := by
calc
∑ i, c i • s i = ∑ i, (c1 i + lam * μ i) • s i := by
refine Finset.sum_congr rfl ?_
intro i _hi
simp [c1, sub_eq_add_neg, add_comm, add_left_comm]
_ = ∑ i, c1 i • s i + ∑ i, (lam * μ i) • s i := by
simp [add_smul, Finset.sum_add_distrib]
_ = ∑ i, c1 i • s i + lam • ∑ i, μ i • s i := by
have hmul :
∑ i, (lam * μ i) • s i = lam • ∑ i, μ i • s i := by
calc
∑ i, (lam * μ i) • s i = ∑ i, lam • (μ i • s i) := by
refine Finset.sum_congr rfl ?_
intro i _hi
simp [mul_smul]
_ = lam • ∑ i, μ i • s i := by
simp [Finset.smul_sum]
simp [hmul]
calc
y = ∑ i, c i • s i := hsum
_ = ∑ i, c1 i • s i + lam • ∑ i, μ i • s i := hsum_expand
_ = ∑ i, c1 i • s i := by
simp [hμsum]
have hsum_filter :
(∑ i, c1 i • s i) =
∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c1 i • s i := by
have hsum_if :
(∑ i, c1 i • s i) = ∑ i, (if i ≠ i0 then c1 i • s i else 0) := by
refine Finset.sum_congr rfl ?_
intro i _hi
by_cases h : i = i0
· subst h
simp [hci0]
· simp [h]
have hsum_filter' :
∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c1 i • s i =
∑ i, (if i ≠ i0 then c1 i • s i else 0) := by
simpa using
(Finset.sum_filter (s := (Finset.univ : Finset (Fin (m + 1))))
(f := fun i => c1 i • s i) (p := fun i => i ≠ i0))
calc
(∑ i, c1 i • s i) = ∑ i, (if i ≠ i0 then c1 i • s i else 0) := hsum_if
_ = ∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c1 i • s i := by
symm
exact hsum_filter'
let I : Type := {i : Fin (m + 1) // i ≠ i0}
have hsum_subtype :
∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c1 i • s i =
∑ i : I, c1 i.1 • s i.1 := by
refine (Finset.sum_subtype (s := Finset.univ.filter (fun i => i ≠ i0))
(p := fun i => i ≠ i0) (f := fun i => c1 i • s i) ?_)
intro i
simp
have hsum_I : y = ∑ i : I, c1 i.1 • s i.1 := by
calc
y = ∑ i, c1 i • s i := hsum_c1
_ = ∑ i ∈ Finset.univ.filter (fun i => i ≠ i0), c1 i • s i := hsum_filter
_ = ∑ i : I, c1 i.1 • s i.1 := hsum_subtype
let e' : Fin m ≃ I := finSuccAboveEquiv i0
let c' : Fin m → Real := fun j => c1 (e' j).1
have hc' : ∀ j, 0 ≤ c' j := by
intro j
simpa [c'] using hc1 (e' j).1
have hsum_equiv :
∑ j, c' j • s (e' j).1 = ∑ i : I, c1 i.1 • s i.1 := by
simpa [c'] using
(Equiv.sum_comp e' (fun i : I => c1 i.1 • s i.1))
let e : Fin m ↪ Fin (m + 1) :=
{ toFun := fun j => (e' j).1
inj' := by
intro j1 j2 h
have h' : e' j1 = e' j2 := by
apply Subtype.ext
simpa using h
exact e'.injective h' }
refine ⟨e, c', hc', ?_⟩
calc
y = ∑ i : I, c1 i.1 • s i.1 := hsum_I
_ = ∑ j, c' j • s (e' j).1 := by
symm
exact hsum_equiv
_ = ∑ j, c' j • s (e j) := rflReduce a nonnegative sum to a linearly independent subfamily.
lemma exists_linearIndependent_nonnegLinearCombination_subfamily {n k : Nat}
{x : Fin n → Real} (v : Fin k → Fin n → Real) (c : Fin k → Real)
(hc : ∀ j, 0 ≤ c j) (hx : x = ∑ j, c j • v j) (hx_ne : x ≠ 0) :
∃ m : Nat, m ≤ k ∧
∃ (e : Fin m ↪ Fin k) (c' : Fin m → Real),
(∀ j, 0 ≤ c' j) ∧
LinearIndependent ℝ (fun j => v (e j)) ∧
x = ∑ j, c' j • v (e j) := by
classical
induction k with
| zero =>
exfalso
have : x = 0 := by
simpa using hx
exact hx_ne this
| succ k ih =>
by_cases hzero : ∃ i : Fin (k + 1), c i = 0
· rcases hzero with ⟨i0, hi0⟩
rcases
drop_zero_coeff_sum_smul_to_shorter_fin
(n := n) (m := k) (s := v) (c := c) hc hx i0 hi0 with
⟨e0, c0, hc0, hx0⟩
rcases
ih (v := fun j => v (e0 j)) (c := c0) (hc := hc0) (hx := hx0) with
⟨m, hm_le, e1, c1, hc1, hlin, hsum⟩
let e : Fin m ↪ Fin (k + 1) :=
{ toFun := fun j => e0 (e1 j)
inj' := by
intro j1 j2 h
exact e1.injective (e0.injective h) }
refine ⟨m, ?_, e, c1, hc1, ?_, ?_⟩
· exact le_trans hm_le (Nat.le_succ k)
· simpa [e] using hlin
· simpa [e] using hsum
· have hpos : ∀ i, 0 < c i := by
intro i
have hne : c i ≠ 0 := by
intro hci
exact hzero ⟨i, hci⟩
exact lt_of_le_of_ne (hc i) (by simpa [eq_comm] using hne)
by_cases hlin : LinearIndependent ℝ v
· refine ⟨k + 1, le_rfl, Function.Embedding.refl _, c, hc, ?_, ?_⟩
· simpa using hlin
· simpa using hx
· rcases
conic_elim_one_generator_pos_to_shorter_fin
(n := n) (m := k) (s := v) (c := c) hpos hx hlin with
⟨e0, c0, hc0, hx0⟩
rcases
ih (v := fun j => v (e0 j)) (c := c0) (hc := hc0) (hx := hx0) with
⟨m, hm_le, e1, c1, hc1, hlin', hsum⟩
let e : Fin m ↪ Fin (k + 1) :=
{ toFun := fun j => e0 (e1 j)
inj' := by
intro j1 j2 h
exact e1.injective (e0.injective h) }
refine ⟨m, ?_, e, c1, hc1, ?_, ?_⟩
· exact le_trans hm_le (Nat.le_succ k)
· simpa [e] using hlin'
· simpa [e] using hsum
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 mem_convexConeGenerated_iUnion_imp_exists_linearIndependent_nonnegLinearCombination_le
{n : Nat} {I : Type*} (Cᵢ : I → Set (Fin n → Real)) (hnonempty : ∀ i, (Cᵢ i).Nonempty)
(hconv : ∀ i, Convex ℝ (Cᵢ i)) {x : Fin n → Real} :
x ∈ convexConeGenerated n (⋃ i, Cᵢ i) →
x ≠ 0 →
∃ m : Nat, m ≤ n ∧
∃ (idx : Fin m → I) (v : Fin m → Fin n → Real) (c : Fin m → Real),
Function.Injective idx ∧ (∀ j, v j ∈ Cᵢ (idx j)) ∧
LinearIndependent ℝ v ∧ (∀ j, 0 ≤ c j) ∧ x = ∑ j, c j • v j := by
classical
intro hx hx_ne
by_cases hI : Nonempty I
· obtain ⟨i0⟩ := hI
have hT : (⋃ i, Cᵢ i).Nonempty := by
rcases hnonempty i0 with ⟨y, hy⟩
refine ⟨y, ?_⟩
exact Set.mem_iUnion.mpr ⟨i0, hy⟩
rcases
mem_convexConeGenerated_imp_exists_nonnegLinearCombination_le
(n := n) (T := ⋃ i, Cᵢ i) (x := x) hT hx with
⟨k, hk_le, v, c, hv, hc, hx_sum⟩
have hmem : ∀ j, ∃ i, v j ∈ Cᵢ i := by
intro j
rcases Set.mem_iUnion.mp (hv j) with ⟨i, hi⟩
exact ⟨i, hi⟩
rcases
coalesce_nonnegLinearCombination_iUnion_to_injective
(Cᵢ := Cᵢ) (hconv := hconv) (v := v) (c := c)
(hc := hc) (hx := hx_sum) hmem with
⟨m, hm_le, idx, v', c', hidx, hv', hc', hx'⟩
rcases
exists_linearIndependent_nonnegLinearCombination_subfamily
(n := n) (k := m) (v := v') (c := c') (hc := hc') (hx := hx')
(hx_ne := hx_ne) with
⟨m', hm'_le, e, c'', hc'', hlin, hx''⟩
let idx' : Fin m' → I := fun j => idx (e j)
have hidx' : Function.Injective idx' := by
intro j1 j2 h
apply e.injective
apply hidx
simpa [idx'] using h
have hv'' : ∀ j, v' (e j) ∈ Cᵢ (idx' j) := by
intro j
simpa [idx'] using hv' (e j)
have hm'_le_n : m' ≤ n := le_trans hm'_le (le_trans hm_le hk_le)
refine ⟨m', hm'_le_n, idx', (fun j => v' (e j)), c'', hidx', hv'', hlin, hc'', ?_⟩
simpa using hx''
· haveI : IsEmpty I := by
exact (not_nonempty_iff.mp hI)
have hunion : (⋃ i, Cᵢ i) = (∅ : Set (Fin n → Real)) := by
ext x
simp
have hx0 : x = 0 := by
have hx' : x ∈ convexConeGenerated n (∅ : Set (Fin n → Real)) := by
simpa [hunion] using hx
have hx'' : x ∈ ({0} : Set (Fin n → Real)) := by
simpa [convexConeGenerated_empty] using hx'
simpa using hx''
exact (hx_ne hx0).elim/- Corollary 17.1.3. Let `{fᵢ | i ∈ I}` be an arbitrary collection of proper convex functions on
`ℝⁿ`, and let `f := convexHullFunctionFamily fᵢ` be the convex hull of the collection. Then, for
every vector `x`,
`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 convex combination in which at most
`n + 1` coefficients are nonzero and the points with nonzero coefficients are affinely
independent. -/
If a convex-weighted EReal sum is not ⊤, then each term is not ⊤.
lemma bdd_toReal_of_sum_ne_top
{n : Nat} {ι : Sort _} {f : ι → (Fin n → Real) → EReal}
(hf : ∀ i, ProperConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) (f i))
{m : Nat} {idx : Fin m → ι} {x' : Fin m → Fin n → Real} {w : Fin m → Real}
(hw : IsConvexWeights m w) (hwnz : ∀ j, w j ≠ 0)
{z : EReal}
(hz : z = ∑ j, ((w j : Real) : EReal) * f (idx j) (x' j)) (hz_top : z ≠ ⊤) :
∀ j, f (idx j) (x' j) ≠ ⊤ := by
classical
rcases hw with ⟨hw_nonneg, _⟩
intro j
by_contra htop
have hpos : 0 < w j := lt_of_le_of_ne (hw_nonneg j) (Ne.symm (hwnz j))
have hposE : (0 : EReal) < (w j : EReal) := (EReal.coe_pos).2 hpos
have hterm_top :
((w j : Real) : EReal) * f (idx j) (x' j) = ⊤ := by
simpa [htop] using (EReal.mul_top_of_pos (x := (w j : EReal)) hposE)
have hsum_ne_bot :
(Finset.univ.erase j).sum
(fun i => ((w i : Real) : EReal) * f (idx i) (x' i)) ≠ ⊥ := by
refine
sum_ne_bot_of_ne_bot (s := Finset.univ.erase j)
(f := fun i => ((w i : Real) : EReal) * f (idx i) (x' i)) ?_
intro i hi
have hne_bot : f (idx i) (x' i) ≠ ⊥ := (hf (idx i)).2.2 (x' i) (by simp)
refine (EReal.mul_ne_bot ((w i : Real) : EReal) (f (idx i) (x' i))).2 ?_
refine ⟨?_, ?_, ?_, ?_⟩
· left
exact EReal.coe_ne_bot _
· right
exact hne_bot
· left
exact EReal.coe_ne_top _
· left
exact (EReal.coe_nonneg).2 (hw_nonneg i)
have hsum_top :
(∑ i, ((w i : Real) : EReal) * f (idx i) (x' i)) = ⊤ := by
have hsum :=
(Finset.add_sum_erase (s := Finset.univ)
(f := fun i => ((w i : Real) : EReal) * f (idx i) (x' i))
(a := j) (h := by simp))
calc
(∑ i, ((w i : Real) : EReal) * f (idx i) (x' i)) =
((w j : Real) : EReal) * f (idx j) (x' j) +
(Finset.univ.erase j).sum
(fun i => ((w i : Real) : EReal) * f (idx i) (x' i)) := by
simpa using hsum.symm
_ = ⊤ := by
simpa [hterm_top] using (EReal.top_add_of_ne_bot hsum_ne_bot)
have hz' : z = ⊤ := by
simpa [hz] using hsum_top
exact hz_top hz'Non-affine-independence yields a nontrivial affine relation.
lemma exists_affine_relation_of_not_affineIndependent {n m : Nat}
{p : Fin (m + 1) → Fin n → Real} (h : ¬ AffineIndependent ℝ p) :
∃ μ : Fin (m + 1) → Real,
(∑ i, μ i = 0) ∧ (∑ i, μ i • p i = 0) ∧ (∃ i, μ i ≠ 0) := by
classical
by_contra hcontra
have hprop :
∀ μ : Fin (m + 1) → Real,
(∑ i, μ i = 0) →
Finset.univ.weightedVSub p μ = (0 : Fin n → Real) →
∀ i, μ i = 0 := by
intro μ hsum hvs
have hcomb : ∑ i, μ i • p i = (0 : Fin n → Real) := by
have hcomb' :
Finset.univ.weightedVSub p μ = ∑ i, μ i • p i := by
simpa using
(Finset.weightedVSub_eq_linear_combination (s := Finset.univ)
(p := p) (w := μ) hsum)
calc
∑ i, μ i • p i = Finset.univ.weightedVSub p μ := by
symm
exact hcomb'
_ = 0 := hvs
by_contra hnot
have hne : ∃ i, μ i ≠ 0 := by
by_contra hne
have hne' : ∀ i, μ i = 0 := by
simpa [not_exists] using hne
exact hnot hne'
exact hcontra ⟨μ, hsum, hcomb, hne⟩
have h_aff : AffineIndependent ℝ p := by
exact (affineIndependent_iff_of_fintype (k := ℝ) (p := p)).2 hprop
exact h h_affA nontrivial affine relation with zero sum has a positive coefficient.
lemma exists_pos_mu_of_sum_eq_zero_of_ne_zero {m : Nat} {μ : Fin (m + 1) → Real}
(hsum : ∑ i, μ i = 0) (hne : ∃ i, μ i ≠ 0) : ∃ i, 0 < μ i := by
classical
by_contra hpos
have hle : ∀ i, μ i ≤ 0 := by
intro i
by_contra hgt
exact hpos ⟨i, lt_of_not_ge hgt⟩
have hsum' : ∑ i, -μ i = 0 := by
simp [Finset.sum_neg_distrib, hsum]
have hzero : ∀ i, -μ i = 0 := by
have hnonneg : ∀ i, 0 ≤ -μ i := by
intro i
exact neg_nonneg.mpr (hle i)
have hzero' :
∀ i ∈ (Finset.univ : Finset (Fin (m + 1))), -μ i = 0 :=
(Finset.sum_eq_zero_iff_of_nonneg
(s := (Finset.univ : Finset (Fin (m + 1))))
(f := fun i => -μ i)
(by intro i hi; exact hnonneg i)).1 hsum'
intro i
exact hzero' i (by simp)
have hzero' : ∀ i, μ i = 0 := by
intro i
have := hzero i
linarith
rcases hne with ⟨i, hi⟩
exact hi (hzero' i)Eliminate one point from a convex combination while not increasing a linear objective.
lemma convex_elim_one_point_obj_to_shorter_fin {n m : Nat}
{p : Fin (m + 1) → Fin n → Real} {w : Fin (m + 1) → Real}
{x : Fin n → Real} {a : Fin (m + 1) → Real}
(hw : IsConvexWeights (m + 1) w) (hwnz : ∀ i, w i ≠ 0)
(hx : x = convexCombination n (m + 1) p w)
(hdep : ¬ AffineIndependent ℝ p) :
∃ (i0 : Fin (m + 1)) (w1 : Fin (m + 1) → Real),
IsConvexWeights (m + 1) w1 ∧
x = convexCombination n (m + 1) p w1 ∧
w1 i0 = 0 ∧
(∑ i, w1 i * a i ≤ ∑ i, w i * a i) := by
classical
rcases hw with ⟨hw_nonneg, hw_sum⟩
obtain ⟨μ, hsumμ, hsumμp, hμne⟩ :=
exists_affine_relation_of_not_affineIndependent (p := p) hdep
let μ' : Fin (m + 1) → Real :=
if 0 ≤ ∑ i, μ i * a i then μ else fun i => -μ i
have hsumμ' : ∑ i, μ' i = 0 := by
by_cases hobj : 0 ≤ ∑ i, μ i * a i
· simp [μ', hobj, hsumμ]
· simp [μ', hobj, hsumμ, Finset.sum_neg_distrib]
have hsumμp' : ∑ i, μ' i • p i = 0 := by
by_cases hobj : 0 ≤ ∑ i, μ i * a i
· simp [μ', hobj, hsumμp]
· simp [μ', hobj, Finset.sum_neg_distrib, hsumμp]
have hμ'ne : ∃ i, μ' i ≠ 0 := by
by_cases hobj : 0 ≤ ∑ i, μ i * a i
· simpa [μ', hobj] using hμne
· simpa [μ', hobj] using hμne
have hobj' : 0 ≤ ∑ i, μ' i * a i := by
by_cases hobj : 0 ≤ ∑ i, μ i * a i
· simp [μ', hobj]
·
have hneg : ∑ i, μ i * a i < 0 := lt_of_not_ge hobj
have hnonneg : 0 ≤ -∑ i, μ i * a i := by linarith
have hsum' : ∑ i, μ' i * a i = -∑ i, μ i * a i := by
calc
∑ i, μ' i * a i = ∑ i, (-μ i) * a i := by simp [μ', hobj]
_ = ∑ i, -(μ i * a i) := by
refine Finset.sum_congr rfl ?_
intro i _hi
simp [neg_mul]
_ = -∑ i, μ i * a i := by
simp [Finset.sum_neg_distrib]
simpa [hsum'] using hnonneg
let P : Finset (Fin (m + 1)) := Finset.univ.filter (fun i => 0 < μ' i)
have hPne : P.Nonempty := by
rcases exists_pos_mu_of_sum_eq_zero_of_ne_zero (μ := μ') hsumμ' hμ'ne with ⟨i, hi⟩
exact ⟨i, by simp [P, hi]⟩
obtain ⟨i0, hi0P, hmin⟩ := Finset.exists_min_image P (fun i => w i / μ' i) hPne
have hμi0 : 0 < μ' i0 := (Finset.mem_filter.mp hi0P).2
have hμi0_ne : μ' i0 ≠ 0 := ne_of_gt hμi0
let t : Real := w i0 / μ' i0
let w1 : Fin (m + 1) → Real := fun i => w i - t * μ' i
have ht_nonneg : 0 ≤ t := by
have hw_pos : 0 < w i0 := lt_of_le_of_ne (hw_nonneg i0) (Ne.symm (hwnz i0))
exact div_nonneg (le_of_lt hw_pos) (le_of_lt hμi0)
have hw1_nonneg : ∀ i, 0 ≤ w1 i := by
intro i
by_cases hμpos_i : 0 < μ' i
· have hi : i ∈ P := by simp [P, hμpos_i]
have hmin_i : t ≤ w i / μ' i := hmin i hi
have hle : t * μ' i ≤ w i := (le_div_iff₀ hμpos_i).1 hmin_i
exact sub_nonneg_of_le hle
· have hμle : μ' i ≤ 0 := le_of_not_gt hμpos_i
have hterm : 0 ≤ -t * μ' i := by
have : 0 ≤ t * (-μ' i) := mul_nonneg ht_nonneg (neg_nonneg.mpr hμle)
simpa [mul_comm, mul_left_comm, mul_assoc, mul_neg, neg_mul] using this
have : 0 ≤ w i + (-t * μ' i) := add_nonneg (hw_nonneg i) hterm
simpa [w1, sub_eq_add_neg] using this
have hw1_sum : ∑ i, w1 i = 1 := by
have hsum_w1 :
∑ i, w1 i = ∑ i, w i - t * ∑ i, μ' i := by
calc
∑ i, w1 i = ∑ i, (w i - t * μ' i) := rfl
_ = ∑ i, w i - ∑ i, t * μ' i := by
simp [Finset.sum_sub_distrib]
_ = ∑ i, w i - t * ∑ i, μ' i := by
have hsum_mul :
∑ i, t * μ' i = t * ∑ i, μ' i := by
simpa using
(Finset.mul_sum (s := (Finset.univ : Finset (Fin (m + 1))))
(f := fun i => μ' i) (a := t)).symm
simp [hsum_mul]
calc
∑ i, w1 i = ∑ i, w i - t * ∑ i, μ' i := hsum_w1
_ = 1 := by simp [hw_sum, hsumμ']
have hw1 : IsConvexWeights (m + 1) w1 := ⟨hw1_nonneg, hw1_sum⟩
have hx1 : x = convexCombination n (m + 1) p w1 := by
have hsum_p :
∑ i, w1 i • p i = ∑ i, w i • p i - t • ∑ i, μ' i • p i := by
calc
∑ i, w1 i • p i = ∑ i, (w i - t * μ' i) • p i := rfl
_ = ∑ i, w i • p i - ∑ i, (t * μ' i) • p i := by
simp [sub_smul, Finset.sum_sub_distrib]
_ = ∑ i, w i • p i - t • ∑ i, μ' i • p i := by
have hsum_smul :
∑ i, (t * μ' i) • p i = t • ∑ i, μ' i • p i := by
have :
t • ∑ i, μ' i • p i = ∑ i, t • (μ' i • p i) := by
simpa using
(Finset.smul_sum (r := t) (s := (Finset.univ : Finset (Fin (m + 1))))
(f := fun i => μ' i • p i))
have := this.symm
simpa [mul_smul] using this
simp [hsum_smul]
have hsum_p' : ∑ i, w1 i • p i = ∑ i, w i • p i := by
simpa [hsumμp'] using hsum_p
have hx_sum : ∑ i, w i • p i = x := by
simpa [convexCombination] using hx.symm
calc
x = ∑ i, w i • p i := by symm; exact hx_sum
_ = ∑ i, w1 i • p i := by symm; exact hsum_p'
_ = convexCombination n (m + 1) p w1 := by simp [convexCombination]
have hw1_i0 : w1 i0 = 0 := by
have hmul : (w i0 / μ' i0) * μ' i0 = w i0 := by
field_simp [hμi0_ne]
simp [w1, t, hmul]
have hobj_le :
∑ i, w1 i * a i ≤ ∑ i, w i * a i := by
have hsum_obj :
∑ i, w1 i * a i = ∑ i, w i * a i - t * ∑ i, μ' i * a i := by
calc
∑ i, w1 i * a i = ∑ i, (w i - t * μ' i) * a i := rfl
_ = ∑ i, (w i * a i - (t * μ' i) * a i) := by
refine Finset.sum_congr rfl ?_
intro i _hi
simpa using (sub_mul (w i) (t * μ' i) (a i))
_ = ∑ i, w i * a i - ∑ i, (t * μ' i) * a i := by
simp [Finset.sum_sub_distrib]
_ = ∑ i, w i * a i - t * ∑ i, μ' i * a i := by
have hsum_mul :
∑ i, (t * μ' i) * a i = t * ∑ i, μ' i * a i := by
have : ∑ i, t * (μ' i * a i) = t * ∑ i, μ' i * a i := by
simpa using
(Finset.mul_sum (s := (Finset.univ : Finset (Fin (m + 1))))
(f := fun i => μ' i * a i) (a := t)).symm
simpa [mul_assoc] using this
simp [hsum_mul]
have hnonneg : 0 ≤ t * ∑ i, μ' i * a i := by
exact mul_nonneg ht_nonneg hobj'
have := sub_le_self (∑ i, w i * a i) hnonneg
simpa [hsum_obj] using this
refine ⟨i0, w1, hw1, hx1, hw1_i0, hobj_le⟩end Section17end Chap04