refactor(analysis/convex/caratheodory): generalize ℝ to an arbitrary linearly ordered field (#9479)

As a result; `convex_independent_iff_finset` also gets generalized.

Author: YaelDillies

src/analysis/convex/caratheodory.lean

@@ -5,7 +5,7 @@ Authors: Johan Commelin, Scott Morrison
 -/
 import analysis.convex.combination
 import linear_algebra.affine_space.independent
-import data.real.basic
+import tactic.field_simp
 
 /-!
 # Carathéodory's convexity theorem
@@ -21,7 +21,7 @@ contains `x`. Thus the difference from the case of affine span is that the affin
 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`.
+in `𝕜ᵈ` is the union of the convex hulls of the `(d + 1)`-tuples in `s`.
 
 ## Main results
 
@@ -36,20 +36,19 @@ convex hull, caratheodory
 
 -/
 
-universes u
-
 open set finset
 open_locale big_operators
 
-variables {E : Type u} [add_comm_group E] [module ℝ E]
+universes u
+variables {𝕜 : Type*} {E : Type u} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E]
 
 namespace caratheodory
 
 /-- 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) :=
+  (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,
@@ -63,7 +62,7 @@ begin
     exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩ },
   have hg   : 0 < g i₀ := by { rw mem_filter at mem, exact mem.2 },
   have hi₀  : i₀ ∈ t   := filter_subset _ _ mem,
-  let  k    : E → ℝ    := λ z, f z - (f i₀ / g i₀) * g z,
+  let  k    : E → 𝕜    := λ z, f z - (f i₀ / g i₀) * g z,
   have hk   : k i₀ = 0 := by field_simp [k, ne_of_gt hg],
   have ksum : ∑ e in t.erase i₀, k e = 1,
   { calc ∑ e in t.erase i₀, k e = ∑ e in t, k e :
@@ -89,36 +88,36 @@ begin
       sub_zero, center_mass, fsum, inv_one, one_smul, id.def] }
 end
 
-variables {s : set E} {x : E} (hx : x ∈ convex_hull ℝ s)
+variables {s : set E} {x : E} (hx : x ∈ convex_hull 𝕜 s)
 include hx
 
 /-- 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) }
+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)
 
 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
+(function.argmin_on_mem _ _ { t : finset E | ↑t ⊆ s ∧ x ∈ convex_hull 𝕜 (t : set E) } _).1
 
 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
+  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
 
 lemma min_card_finset_of_mem_convex_hull_nonempty :
   (min_card_finset_of_mem_convex_hull hx).nonempty :=
 begin
-  rw [← finset.coe_nonempty, ← @convex_hull_nonempty_iff ℝ],
+  rw [← finset.coe_nonempty, ← @convex_hull_nonempty_iff 𝕜],
   exact ⟨x, mem_min_card_finset_of_mem_convex_hull hx⟩,
 end
 
 lemma min_card_finset_of_mem_convex_hull_card_le_card
-  {t : finset E} (ht₁ : ↑t ⊆ s) (ht₂ : x ∈ convex_hull ℝ (t : set E)) :
+  {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₂⟩
 
 lemma affine_independent_min_card_finset_of_mem_convex_hull :
-  affine_independent ℝ (coe : min_card_finset_of_mem_convex_hull hx → E) :=
+  affine_independent 𝕜 (coe : min_card_finset_of_mem_convex_hull hx → E) :=
 begin
   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,
@@ -142,8 +141,8 @@ 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 :=
+  convex_hull 𝕜 s =
+  ⋃ (t : finset E) (hss : ↑t ⊆ s) (hai : affine_independent 𝕜 (coe : t → E)), convex_hull 𝕜 ↑t :=
 begin
   apply set.subset.antisymm,
   { intros x hx,
@@ -157,9 +156,9 @@ begin
 end
 
 /-- 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)
+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
   rw convex_hull_eq_union at hx,

src/analysis/convex/extreme.lean

@@ -8,7 +8,7 @@ import analysis.convex.hull
 /-!
 # Extreme sets
 
-This file defines extreme sets and extreme points for sets in a real vector space.
+This file defines extreme sets and extreme points for sets in a module.
 
 An extreme set of `A` is a subset of `A` that is as far as it can get in any outward direction: If
 point `x` is in it and point `y ∈ A`, then the line passing through `x` and `y` leaves `A` at `x`.

src/analysis/convex/independent.lean

@@ -42,10 +42,10 @@ independence, convex position
 
 open_locale affine big_operators classical
 open finset function
-variables (𝕜 : Type*) {E : Type*}
+variables {𝕜 E ι : Type*}
 
 section ordered_semiring
-variables [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {ι : Type*} {s t : set E}
+variables (𝕜) [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {s t : set E}
 
 /-- An indexed family is said to be convex independent if every point only belongs to convex hulls
 of sets containing it. -/
@@ -54,34 +54,6 @@ def convex_independent (p : ι → E) : Prop :=
 
 variables {𝕜}
 
-/-- To check convex independence, one only has to check finsets thanks to Carathéodory's theorem. -/
-lemma convex_independent_iff_finset [module ℝ E] {p : ι → E} :
-  convex_independent ℝ p
-  ↔ ∀ (s : finset ι) (x : ι), p x ∈ convex_hull ℝ (s.image p : set E) → x ∈ s :=
-begin
-  refine ⟨λ hc s x hx, hc s x _, λ h s x hx, _⟩,
-  { rwa finset.coe_image at hx },
-  have hp : injective p,
-  { rintro a b hab,
-    rw ←mem_singleton,
-    refine h {b} a _,
-    rw [hab, image_singleton, coe_singleton, convex_hull_singleton],
-    exact set.mem_singleton _ },
-  let s' : finset ι :=
-    (caratheodory.min_card_finset_of_mem_convex_hull hx).preimage p (hp.inj_on _),
-  suffices hs' : x ∈ s',
-  { rw ←hp.mem_set_image,
-    rw [finset.mem_preimage, ←mem_coe] at hs',
-    exact caratheodory.min_card_finset_of_mem_convex_hull_subseteq hx hs' },
-  refine h s' x _,
-  have : s'.image p = caratheodory.min_card_finset_of_mem_convex_hull hx,
-  { rw [image_preimage, filter_true_of_mem],
-    exact λ y hy, set.image_subset_range _ s
-      (caratheodory.min_card_finset_of_mem_convex_hull_subseteq hx $ mem_coe.2 hy) },
-  rw this,
-  exact caratheodory.mem_min_card_finset_of_mem_convex_hull hx,
-end
-
 /-- A family with at most one point is convex independent. -/
 lemma subsingleton.convex_independent [subsingleton ι] (p : ι → E) :
   convex_independent 𝕜 p :=
@@ -193,11 +165,39 @@ end
 
 end ordered_semiring
 
-/-! ### Extreme points -/
-
 section linear_ordered_field
 variables [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E}
 
+/-- To check convex independence, one only has to check finsets thanks to Carathéodory's theorem. -/
+lemma convex_independent_iff_finset {p : ι → E} :
+  convex_independent 𝕜 p
+  ↔ ∀ (s : finset ι) (x : ι), p x ∈ convex_hull 𝕜 (s.image p : set E) → x ∈ s :=
+begin
+  refine ⟨λ hc s x hx, hc s x _, λ h s x hx, _⟩,
+  { rwa finset.coe_image at hx },
+  have hp : injective p,
+  { rintro a b hab,
+    rw ←mem_singleton,
+    refine h {b} a _,
+    rw [hab, image_singleton, coe_singleton, convex_hull_singleton],
+    exact set.mem_singleton _ },
+  let s' : finset ι :=
+    (caratheodory.min_card_finset_of_mem_convex_hull hx).preimage p (hp.inj_on _),
+  suffices hs' : x ∈ s',
+  { rw ←hp.mem_set_image,
+    rw [finset.mem_preimage, ←mem_coe] at hs',
+    exact caratheodory.min_card_finset_of_mem_convex_hull_subseteq hx hs' },
+  refine h s' x _,
+  have : s'.image p = caratheodory.min_card_finset_of_mem_convex_hull hx,
+  { rw [image_preimage, filter_true_of_mem],
+    exact λ y hy, set.image_subset_range _ s
+      (caratheodory.min_card_finset_of_mem_convex_hull_subseteq hx $ mem_coe.2 hy) },
+  rw this,
+  exact caratheodory.mem_min_card_finset_of_mem_convex_hull hx,
+end
+
+/-! ### Extreme points -/
+
 lemma convex.convex_independent_extreme_points (hs : convex 𝕜 s) :
   convex_independent 𝕜 (λ p, p : s.extreme_points 𝕜 → E) :=
 convex_independent_set_iff_not_mem_convex_hull_diff.2 $ λ x hx h,