feat(analysis/convex/caratheodory): strengthen Caratheodory's lemma to provide affine independence (#8892)

The changes here are:

- Use hypothesis `¬ affine_independent ℝ (coe : t → E)` instead of `finrank ℝ E + 1 < t.card`
- Drop no-longer-necessary `[finite_dimensional ℝ E]` assumption
- Do not use a shrinking argument but start by choosing an appropriate subset of minimum cardinality via `min_card_finset_of_mem_convex_hull`
- Provide a single alternative form of Carathéodory's lemma `eq_pos_convex_span_of_mem_convex_hull`
- In the alternate form, define the explicit linear combination using elements parameterised by a new `fintype` rather than on the entire ambient space `E` (we thus avoid the issue of junk values outside of the relevant subset)

Author: ocfnash

src/analysis/convex/caratheodory.lean

@@ -4,14 +4,25 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Scott Morrison
 -/
 import analysis.convex.basic
+import linear_algebra.affine_space.independent
 
 /-!
 # Carathéodory's convexity theorem
 
-This file is devoted to proving Carathéodory's convexity theorem:
-The convex hull of a set `s` in ℝᵈ is the union of the convex hulls of the (d+1)-tuples in `s`.
+Convex hull can be regarded as a refinement of affine span. Both are closure operators but whereas
+convex hull takes values in the lattice of convex subsets, affine span takes values in the much
+coarser sublattice of affine subspaces.
 
-## Main results:
+The cost of this refinement is that one no longer has bases. However Carathéodory's convexity
+theorem offers some compensation. Given a set `s` together with a point `x` in its convex hull,
+Carathéodory says that one may find an affine-independent family of elements `s` whose convex hull
+contains `x`. Thus the difference from the case of affine span is that the affine-independent family
+depends on `x`.
+
+In particular, in finite dimensions Carathéodory's theorem implies that the convex hull of a set `s`
+in `ℝᵈ` is the union of the convex hulls of the `(d+1)`-tuples in `s`.
+
+## Main results
 
 * `convex_hull_eq_union`: Carathéodory's convexity theorem
 
@@ -26,24 +37,23 @@ convex hull, caratheodory
 
 universes u
 
-open set finset finite_dimensional
+open set finset
 open_locale big_operators
 
-variables {E : Type u} [add_comm_group E] [module ℝ E] [finite_dimensional ℝ E]
+variables {E : Type u} [add_comm_group E] [module ℝ E]
 
 namespace caratheodory
 
-/--
-If `x` is in the convex hull of some finset `t` with strictly more than `finrank + 1` elements,
-then it is in the union of the convex hulls of the finsets `t.erase y` for `y ∈ t`.
--/
-lemma mem_convex_hull_erase [decidable_eq E] {t : finset E} (h : finrank ℝ E + 1 < t.card)
-  {x : E} (m : x ∈ convex_hull (↑t : set E)) :
+/-- If `x` is in the convex hull of some finset `t` whose elements are not affine-independent,
+then it is in the convex hull of a strict subset of `t`. -/
+lemma mem_convex_hull_erase [decidable_eq E] {t : finset E}
+  (h : ¬ affine_independent ℝ (coe : t → E)) {x : E} (m : x ∈ convex_hull (↑t : set E)) :
   ∃ (y : (↑t : set E)), x ∈ convex_hull (↑(t.erase y) : set E) :=
 begin
   simp only [finset.convex_hull_eq, mem_set_of_eq] at m ⊢,
   obtain ⟨f, fpos, fsum, rfl⟩ := m,
-  obtain ⟨g, gcombo, gsum, gpos⟩ := exists_relation_sum_zero_pos_coefficient_of_dim_succ_lt_card h,
+  obtain ⟨g, gcombo, gsum, gpos⟩ := exists_nontrivial_relation_sum_zero_of_not_affine_ind h,
+  replace gpos := exists_pos_of_sum_zero_of_exists_nonzero g gsum gpos,
   clear h,
   let s := t.filter (λ z : E, 0 < g z),
   obtain ⟨i₀, mem, w⟩ : ∃ i₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i,
@@ -78,148 +88,97 @@ begin
       sub_zero, center_mass, fsum, inv_one, one_smul, id.def], },
 end
 
-/--
-The convex hull of a finset `t` with `finrank ℝ E + 1 < t.card` is equal to
-the union of the convex hulls of the finsets `t.erase x` for `x ∈ t`.
--/
-lemma step [decidable_eq E] (t : finset E) (h : finrank ℝ E + 1 < t.card) :
-  convex_hull (↑t : set E) = ⋃ (x : (↑t : set E)), convex_hull ↑(t.erase x) :=
-begin
-  apply set.subset.antisymm,
-  { intros x m',
-    obtain ⟨y, m⟩ := mem_convex_hull_erase h m',
-    exact mem_Union.2 ⟨y, m⟩, },
-  { refine Union_subset _,
-    intro x,
-    apply convex_hull_mono,
-    apply erase_subset, }
-end
+variables {s : set E} {x : E} (hx : x ∈ convex_hull s)
+include hx
 
-/--
-The convex hull of a finset `t` with `finrank ℝ E + 1 < t.card` is contained in
-the union of the convex hulls of the finsets `t' ⊆ t` with `t'.card ≤ finrank ℝ E + 1`.
--/
-lemma shrink' (t : finset E) (k : ℕ) (h : t.card = finrank ℝ E + 1 + k) :
-  convex_hull (↑t : set E) ⊆
-    ⋃ (t' : finset E) (w : t' ⊆ t) (b : t'.card ≤ finrank ℝ E + 1), convex_hull ↑t' :=
-begin
-  induction k with k ih generalizing t,
-  { apply subset_subset_Union t,
-    apply subset_subset_Union (set.subset.refl _),
-    exact subset_subset_Union (le_of_eq h) (subset.refl _), },
-  { classical,
-    rw step _ (by { rw h, simp, } : finrank ℝ E + 1 < t.card),
-    apply Union_subset,
-    intro i,
-    transitivity,
-    { apply ih,
-      rw [card_erase_of_mem, h, nat.add_succ, nat.pred_succ],
-      exact i.2, },
-    { apply Union_subset_Union,
-      intro t',
-      apply Union_subset_Union_const,
-      exact λ h, set.subset.trans h (erase_subset _ _), } }
-end
+/-- Given a point `x` in the convex hull of a set `s`, this is a finite subset of `s` of minimum
+cardinality, whose convex hull contains `x`. -/
+noncomputable def min_card_finset_of_mem_convex_hull : finset E :=
+function.argmin_on finset.card nat.lt_wf { t | ↑t ⊆ s ∧ x ∈ convex_hull (t : set E) }
+(by simpa only [convex_hull_eq_union_convex_hull_finite_subsets s, exists_prop, mem_Union] using hx)
 
-/--
-The convex hull of any finset `t` is contained in
-the union of the convex hulls of the finsets `t' ⊆ t` with `t'.card ≤ finrank ℝ E + 1`.
--/
-lemma shrink (t : finset E) :
-  convex_hull (↑t : set E) ⊆
-    ⋃ (t' : finset E) (w : t' ⊆ t) (b : t'.card ≤ finrank ℝ E + 1), convex_hull ↑t' :=
-begin
-  by_cases h : t.card ≤ finrank ℝ E + 1,
-  { apply subset_subset_Union t,
-    apply subset_subset_Union (set.subset.refl _),
-    exact subset_subset_Union h (set.subset.refl _), },
-  push_neg at h,
-  obtain ⟨k, w⟩ := le_iff_exists_add.mp (le_of_lt h), clear h,
-  exact shrink' _ _ w,
-end
+lemma min_card_finset_of_mem_convex_hull_subseteq : ↑(min_card_finset_of_mem_convex_hull hx) ⊆ s :=
+(function.argmin_on_mem _ _ { t : finset E | ↑t ⊆ s ∧ x ∈ convex_hull (t : set E) } _).1
 
-end caratheodory
-
-/--
-One inclusion of **Carathéodory's convexity theorem**.
+lemma mem_min_card_finset_of_mem_convex_hull :
+  x ∈ convex_hull (min_card_finset_of_mem_convex_hull hx : set E) :=
+(function.argmin_on_mem _ _ { t : finset E | ↑t ⊆ s ∧ x ∈ convex_hull (t : set E) } _).2
 
-The convex hull of a set `s` in ℝᵈ is contained in
-the union of the convex hulls of the (d+1)-tuples in `s`.
--/
-lemma convex_hull_subset_union (s : set E) :
-  convex_hull s ⊆ ⋃ (t : finset E) (w : ↑t ⊆ s) (b : t.card ≤ finrank ℝ E + 1), convex_hull ↑t :=
+lemma min_card_finset_of_mem_convex_hull_nonempty :
+  (min_card_finset_of_mem_convex_hull hx).nonempty :=
 begin
-  -- First we replace `convex_hull s` with the union of the convex hulls of finite subsets,
-  rw convex_hull_eq_union_convex_hull_finite_subsets,
-  -- and prove the inclusion for each of those.
-  apply Union_subset, intro r,
-  apply Union_subset, intro h,
-  -- Second, for each convex hull of a finite subset, we shrink it.
-  refine subset.trans (caratheodory.shrink _) _,
-  -- After that it's just shuffling unions around.
-  refine Union_subset_Union (λ t, _),
-  exact Union_subset_Union2 (λ htr, ⟨subset.trans htr h, subset.refl _⟩)
+  rw [← finset.coe_nonempty, ← convex_hull_nonempty_iff],
+  exact ⟨x, mem_min_card_finset_of_mem_convex_hull hx⟩,
 end
 
-/--
-**Carathéodory's convexity theorem**.
+lemma min_card_finset_of_mem_convex_hull_card_le_card
+  {t : finset E} (ht₁ : ↑t ⊆ s) (ht₂ : x ∈ convex_hull (t : set E)) :
+  (min_card_finset_of_mem_convex_hull hx).card ≤ t.card :=
+function.argmin_on_le _ _ _ ⟨ht₁, ht₂⟩
 
-The convex hull of a set `s` in ℝᵈ is the union of the convex hulls of the (d+1)-tuples in `s`.
--/
-theorem convex_hull_eq_union (s : set E) :
-  convex_hull s = ⋃ (t : finset E) (w : ↑t ⊆ s) (b : t.card ≤ finrank ℝ E + 1), convex_hull ↑t :=
+lemma affine_independent_min_card_finset_of_mem_convex_hull :
+  affine_independent ℝ (coe : min_card_finset_of_mem_convex_hull hx → E) :=
 begin
-  apply set.subset.antisymm,
-  { apply convex_hull_subset_union, },
-  iterate 3 { convert Union_subset _, intro, },
-  exact convex_hull_mono ‹_›,
+  let k := (min_card_finset_of_mem_convex_hull hx).card - 1,
+  have hk : (min_card_finset_of_mem_convex_hull hx).card = k + 1,
+  { exact (nat.succ_pred_eq_of_pos
+      (finset.card_pos.mpr (min_card_finset_of_mem_convex_hull_nonempty hx))).symm, },
+  classical,
+  by_contra,
+  obtain ⟨p, hp⟩ := mem_convex_hull_erase h (mem_min_card_finset_of_mem_convex_hull hx),
+  have contra := min_card_finset_of_mem_convex_hull_card_le_card hx (set.subset.trans
+    (finset.erase_subset ↑p (min_card_finset_of_mem_convex_hull hx))
+    (min_card_finset_of_mem_convex_hull_subseteq hx)) hp,
+  rw [← not_lt] at contra,
+  apply contra,
+  erw [card_erase_of_mem p.2, hk],
+  exact lt_add_one _,
 end
 
-/--
-A more explicit formulation of **Carathéodory's convexity theorem**,
-writing an element of a convex hull as the center of mass
-of an explicit `finset` with cardinality at most `dim + 1`.
--/
-theorem eq_center_mass_card_le_dim_succ_of_mem_convex_hull
-  {s : set E} {x : E} (h : x ∈ convex_hull s) :
-  ∃ (t : finset E) (w : ↑t ⊆ s) (b : t.card ≤ finrank ℝ E + 1)
-    (f : E → ℝ), (∀ y ∈ t, 0 ≤ f y) ∧ t.sum f = 1 ∧ t.center_mass f id = x :=
+end caratheodory
+
+variables {s : set E}
+
+/-- **Carathéodory's convexity theorem** -/
+lemma convex_hull_eq_union :
+  convex_hull s =
+  ⋃ (t : finset E) (hss : ↑t ⊆ s) (hai : affine_independent ℝ (coe : t → E)), convex_hull ↑t :=
 begin
-  rw convex_hull_eq_union at h,
-  simp only [exists_prop, mem_Union] at h,
-  obtain ⟨t, w, b, m⟩ := h,
-  refine ⟨t, w, b, _⟩,
-  rw finset.convex_hull_eq at m,
-  simpa only [exists_prop] using m,
+  apply set.subset.antisymm,
+  { intros x hx,
+    simp only [exists_prop, set.mem_Union],
+    exact ⟨caratheodory.min_card_finset_of_mem_convex_hull hx,
+           caratheodory.min_card_finset_of_mem_convex_hull_subseteq hx,
+           caratheodory.affine_independent_min_card_finset_of_mem_convex_hull hx,
+           caratheodory.mem_min_card_finset_of_mem_convex_hull hx⟩, },
+  { iterate 3 { convert set.Union_subset _, intro, },
+    exact convex_hull_mono ‹_›, },
 end
 
-/--
-A variation on **Carathéodory's convexity theorem**,
-writing an element of a convex hull as a center of mass
-of an explicit `finset` with cardinality at most `dim + 1`,
-where all coefficients in the center of mass formula
-are strictly positive.
-
-(This is proved using `eq_center_mass_card_le_dim_succ_of_mem_convex_hull`,
-and discarding any elements of the set with coefficient zero.)
--/
-theorem eq_pos_center_mass_card_le_dim_succ_of_mem_convex_hull
-  {s : set E} {x : E} (h : x ∈ convex_hull s) :
-  ∃ (t : finset E) (w : ↑t ⊆ s) (b : t.card ≤ finrank ℝ E + 1)
-    (f : E → ℝ), (∀ y ∈ t, 0 < f y) ∧ t.sum f = 1 ∧ t.center_mass f id = x :=
+/-- A more explicit version of `convex_hull_eq_union`. -/
+theorem eq_pos_convex_span_of_mem_convex_hull {x : E} (hx : x ∈ convex_hull s) :
+  ∃ (ι : Sort (u+1)) [fintype ι], by exactI ∃ (z : ι → E) (w : ι → ℝ)
+    (hss : set.range z ⊆ s) (hai : affine_independent ℝ z)
+    (hw : ∀ i, 0 < w i), ∑ i, w i = 1 ∧ ∑ i, w i • z i = x :=
 begin
-  obtain ⟨t, w, b, f, ⟨pos, sum, center⟩⟩ := eq_center_mass_card_le_dim_succ_of_mem_convex_hull h,
-  let t' := t.filter (λ z, 0 < f z),
-  have t'sum : t'.sum f = 1,
-  { rw ← sum,
-    exact sum_filter_of_ne (λ x hxt hfx, (pos x hxt).lt_of_ne hfx.symm) },
-  refine ⟨t', _, _, f, ⟨_, t'sum, _⟩⟩,
-  { exact subset.trans (filter_subset _ t) w, },
-  { exact (card_filter_le _ _).trans b, },
-  { exact λ y H, (mem_filter.mp H).right, },
-  { rw ← center,
-    simp only [center_mass, t'sum, sum, inv_one, one_smul, id.def],
-    refine sum_filter_of_ne (λ x hxt hfx, (pos x hxt).lt_of_ne $ λ hf₀, _),
-    rw [← hf₀, zero_smul] at hfx,
-    exact hfx rfl },
+  rw convex_hull_eq_union at hx,
+  simp only [exists_prop, set.mem_Union] at hx,
+  obtain ⟨t, ht₁, ht₂, ht₃⟩ := hx,
+  simp only [t.convex_hull_eq, exists_prop, set.mem_set_of_eq] at ht₃,
+  obtain ⟨w, hw₁, hw₂, hw₃⟩ := ht₃,
+  let t' := t.filter (λ i, w i ≠ 0),
+  refine ⟨t', t'.fintype_coe_sort, (coe : t' → E), w ∘ (coe : t' → E), _, _, _, _, _⟩,
+  { rw subtype.range_coe_subtype, exact set.subset.trans (finset.filter_subset _ t) ht₁, },
+  { exact affine_independent_embedding_of_affine_independent
+      ⟨_, inclusion_injective (finset.filter_subset (λ i, w i ≠ 0) t)⟩ ht₂, },
+  { intros i, suffices : w i ≠ 0,
+    { cases this.lt_or_lt with hneg hpos,
+      { exfalso, rw ← not_le at hneg, apply hneg, exact hw₁ _ (finset.mem_filter.mp i.2).1, },
+      { exact hpos, }, },
+    exact (finset.mem_filter.mp i.property).2, },
+  { erw [finset.sum_attach, finset.sum_filter_ne_zero, hw₂], },
+  { change ∑ (i : t') in t'.attach, (λ e, w e • e) ↑i = x,
+    erw [finset.sum_attach, finset.sum_filter_of_ne],
+    { rw t.center_mass_eq_of_sum_1 id hw₂ at hw₃, exact hw₃, },
+    { intros e he hwe contra, apply hwe, rw [contra, zero_smul], }, },
 end

src/linear_algebra/affine_space/independent.lean

@@ -381,6 +381,24 @@ lemma not_mem_affine_span_diff_of_affine_independent [nontrivial k] {p : ι →
   p i ∉ affine_span k (p '' (s \ {i})) :=
 by simp [ha]
 
+lemma exists_nontrivial_relation_sum_zero_of_not_affine_ind
+  {t : finset V} (h : ¬ affine_independent k (coe : t → V)) :
+  ∃ f : V → k, ∑ e in t, f e • e = 0 ∧ ∑ e in t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0 :=
+begin
+  classical,
+  rw affine_independent_iff_of_fintype at h,
+  simp only [exists_prop, not_forall] at h,
+  obtain ⟨w, hw, hwt, i, hi⟩ := h,
+  simp only [finset.weighted_vsub_eq_weighted_vsub_of_point_of_sum_eq_zero _ w (coe : t → V) hw 0,
+    vsub_eq_sub, finset.weighted_vsub_of_point_apply, sub_zero] at hwt,
+  let f : Π (x : V), x ∈ t → k := λ x hx, w ⟨x, hx⟩,
+  refine ⟨λ x, if hx : x ∈ t then f x hx else (0 : k), _, _, by { use i, simp [hi, f], }⟩,
+  suffices : ∑ (e : V) in t, dite (e ∈ t) (λ hx, (f e hx) • e) (λ hx, 0) = 0,
+  { convert this, ext, by_cases hx : x ∈ t; simp [hx], },
+  all_goals
+  { simp only [finset.sum_dite_of_true (λx h, h), subtype.val_eq_coe, finset.mk_coe, f, hwt, hw], },
+end
+
 end affine_independent
 
 section field