From 257d1b7c0e5bd4baf3032c265c92d709d685d338 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 11 Jun 2020 18:53:58 +0000
Subject: [PATCH] feat(*): preparations for Caratheodory's convexity theorem
 (#3030)

---
 src/algebra/big_operators.lean    | 11 +++++++
 src/algebra/ordered_field.lean    |  2 +-
 src/data/equiv/basic.lean         | 40 ++++++++++++++++++++++++++
 src/data/finset.lean              | 14 +++++++++
 src/data/set/basic.lean           |  3 ++
 src/data/set/finite.lean          |  4 +++
 src/data/set/lattice.lean         |  6 ++++
 src/linear_algebra/basis.lean     | 32 ++++++++++++++++++++-
 src/linear_algebra/dimension.lean | 48 ++++++++++++++++++++++---------
 src/logic/embedding.lean          |  8 ++++++
 10 files changed, 152 insertions(+), 16 deletions(-)

diff --git a/src/algebra/big_operators.lean b/src/algebra/big_operators.lean
index 6fb7bff17aa53..a4fb7fde6ba6f 100644
--- a/src/algebra/big_operators.lean
+++ b/src/algebra/big_operators.lean
@@ -1152,6 +1152,17 @@ begin
   exact sum_lt_sum (λ i hi, le_of_lt (Hlt i hi)) ⟨i, hi, Hlt i hi⟩
 end
 
+lemma exists_pos_of_sum_zero_of_exists_nonzero (f : α → β)
+  (h₁ : ∑ e in s, f e = 0) (h₂ : ∃ x ∈ s, f x ≠ 0) :
+  ∃ x ∈ s, 0 < f x :=
+begin
+  contrapose! h₁,
+  obtain ⟨x, m, x_nz⟩ : ∃ x ∈ s, f x ≠ 0 := h₂,
+  apply ne_of_lt,
+  calc ∑ e in s, f e < ∑ e in s, 0 : by { apply sum_lt_sum h₁ ⟨x, m, lt_of_le_of_ne (h₁ x m) x_nz⟩ }
+                 ... = 0           : by rw [finset.sum_const, nsmul_zero],
+end
+
 end decidable_linear_ordered_cancel_comm_monoid
 
 section linear_ordered_comm_ring
diff --git a/src/algebra/ordered_field.lean b/src/algebra/ordered_field.lean
index 730903ed5b09b..347c826d3d4f7 100644
--- a/src/algebra/ordered_field.lean
+++ b/src/algebra/ordered_field.lean
@@ -11,7 +11,7 @@ set_option old_structure_cmd true
 
 variable {α : Type*}
 
-@[protect_proj] class linear_ordered_field (α : Type*) extends linear_ordered_ring α, field α
+@[protect_proj] class linear_ordered_field (α : Type*) extends linear_ordered_comm_ring α, field α
 
 section linear_ordered_field
 variables [linear_ordered_field α] {a b c d e : α}
diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index a122f18edf467..c3873dcffc713 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -1058,6 +1058,39 @@ lemma sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} [decidable_pred
 have ↑(⟨x, or.inr hx⟩ : (s ∪ -s : set α)) ∈ -s, from hx,
 by { rw [equiv.set.sum_compl], simpa using set.union_apply_right _ this }
 
+/-- `sum_diff_subset s t` is the natural equivalence between
+`s ⊕ (t \ s)` and `t`, where `s` and `t` are two sets. -/
+protected def sum_diff_subset {α} {s t : set α} (h : s ⊆ t) [decidable_pred s] :
+  s ⊕ (t \ s : set α) ≃ t :=
+calc s ⊕ (t \ s : set α) ≃ (s ∪ (t \ s) : set α) : (equiv.set.union (by simp [inter_diff_self])).symm
+... ≃ t : equiv.set.of_eq (by { simp [union_diff_self, union_eq_self_of_subset_left h] })
+
+@[simp] lemma sum_diff_subset_apply_inl
+  {α} {s t : set α} (h : s ⊆ t) [decidable_pred s] (x : s) :
+  equiv.set.sum_diff_subset h (sum.inl x) = inclusion h x := rfl
+
+@[simp] lemma sum_diff_subset_apply_inr
+  {α} {s t : set α} (h : s ⊆ t) [decidable_pred s] (x : t \ s) :
+  equiv.set.sum_diff_subset h (sum.inr x) = inclusion (diff_subset t s) x := rfl
+
+lemma sum_diff_subset_symm_apply_of_mem
+  {α} {s t : set α} (h : s ⊆ t) [decidable_pred s] {x : t} (hx : x.1 ∈ s) :
+  (equiv.set.sum_diff_subset h).symm x = sum.inl ⟨x, hx⟩ :=
+begin
+  apply (equiv.set.sum_diff_subset h).injective,
+  simp only [apply_symm_apply, sum_diff_subset_apply_inl],
+  exact subtype.eq rfl,
+end
+
+lemma sum_diff_subset_symm_apply_of_not_mem
+  {α} {s t : set α} (h : s ⊆ t) [decidable_pred s] {x : t} (hx : x.1 ∉ s) :
+  (equiv.set.sum_diff_subset h).symm x = sum.inr ⟨x, ⟨x.2, hx⟩⟩  :=
+begin
+  apply (equiv.set.sum_diff_subset h).injective,
+  simp only [apply_symm_apply, sum_diff_subset_apply_inr],
+  exact subtype.eq rfl,
+end
+
 /-- If `s` is a set with decidable membership, then the sum of `s ∪ t` and `s ∩ t` is equivalent
 to `s ⊕ t`. -/
 protected def union_sum_inter {α : Type u} (s t : set α) [decidable_pred s] :
@@ -1105,6 +1138,13 @@ protected noncomputable def range {α β} (f : α → β) (H : injective f) :
 @[simp] theorem range_apply {α β} (f : α → β) (H : injective f) (a) :
   set.range f H a = ⟨f a, set.mem_range_self _⟩ := rfl
 
+theorem apply_range_symm {α β} (f : α → β) (H : injective f) (b : range f) :
+  f ((set.range f H).symm b) = b :=
+begin
+  conv_rhs { rw ←((set.range f H).right_inv b), },
+  simp,
+end
+
 /-- If `α` is equivalent to `β`, then `set α` is equivalent to `set β`. -/
 protected def congr {α β : Type*} (e : α ≃ β) : set α ≃ set β :=
 ⟨λ s, e '' s, λ t, e.symm '' t, symm_image_image e, symm_image_image e.symm⟩
diff --git a/src/data/finset.lean b/src/data/finset.lean
index 9a285388123d7..8f7d88a6bcfa8 100644
--- a/src/data/finset.lean
+++ b/src/data/finset.lean
@@ -53,6 +53,12 @@ instance : has_lift (finset α) (set α) := ⟨λ s, {x | x ∈ s}⟩
 
 @[simp] lemma set_of_mem {α} {s : finset α} : {a | a ∈ s} = ↑s := rfl
 
+@[simp] lemma coe_mem {s : finset α} (x : (↑s : set α)) : ↑x ∈ s := x.2
+
+@[simp] lemma mk_coe {s : finset α} (x : (↑s : set α)) {h} :
+  (⟨↑x, h⟩ : (↑s : set α)) = x :=
+by { apply subtype.eq, refl, }
+
 instance decidable_mem' [decidable_eq α] (a : α) (s : finset α) :
   decidable (a ∈ (↑s : set α)) := s.decidable_mem _
 
@@ -966,6 +972,14 @@ lemma filter_eq' [decidable_eq β] (s : finset β) (b : β) :
   s.filter (λ a, a = b) = ite (b ∈ s) {b} ∅ :=
 trans (filter_congr (λ _ _, ⟨eq.symm, eq.symm⟩)) (filter_eq s b)
 
+lemma filter_ne [decidable_eq β] (s : finset β) (b : β) :
+  s.filter (λ a, b ≠ a) = s.erase b :=
+by { ext, simp only [mem_filter, mem_erase, ne.def], cc, }
+
+lemma filter_ne' [decidable_eq β] (s : finset β) (b : β) :
+  s.filter (λ a, a ≠ b) = s.erase b :=
+trans (filter_congr (λ _ _, ⟨ne.symm, ne.symm⟩)) (filter_ne s b)
+
 end filter
 
 /-! ### range -/
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 2b446a7dd3874..8134bb5288d5e 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -1725,6 +1725,9 @@ def inclusion {s t : set α} (h : s ⊆ t) : s → t :=
   (x : s) : inclusion htu (inclusion hst x) = inclusion (set.subset.trans hst htu) x :=
 by cases x; refl
 
+@[simp] lemma coe_inclusion {s t : set α} (h : s ⊆ t) (x : s) :
+  (inclusion h x : α) = (x : α) := rfl
+
 lemma inclusion_injective {s t : set α} (h : s ⊆ t) :
   function.injective (inclusion h)
 | ⟨_, _⟩ ⟨_, _⟩ := subtype.ext.2 ∘ subtype.ext.1
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index 29a73ef1d8cde..033e02cfd9976 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -359,6 +359,10 @@ set.finite_mem_finset s
 @[simp] lemma coe_bind {f : α → finset β} : ↑(s.bind f) = (⋃x ∈ (↑s : set α), ↑(f x) : set β) :=
 by simp [set.ext_iff]
 
+@[simp] lemma finite_to_set_to_finset {α : Type*} (s : finset α) :
+  (finite_to_set s).to_finset = s :=
+by { ext, rw [set.finite.mem_to_finset, mem_coe] }
+
 end finset
 
 namespace set
diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean
index 330da74a98081..1f206a3ee488c 100644
--- a/src/data/set/lattice.lean
+++ b/src/data/set/lattice.lean
@@ -112,6 +112,12 @@ theorem subset_Inter {t : set β} {s : ι → set β} (h : ∀ i, t ⊆ s i) : t
 
 theorem subset_Union : ∀ (s : ι → set β) (i : ι), s i ⊆ (⋃ i, s i) := le_supr
 
+-- This rather trivial consequence is convenient with `apply`,
+-- and has `i` explicit for this use case.
+theorem subset_subset_Union
+  {A : set β} {s : ι → set β} (i : ι) (h : A ⊆ s i) : A ⊆ ⋃ (i : ι), s i :=
+subset.trans h (subset_Union s i)
+
 theorem Inter_subset : ∀ (s : ι → set β) (i : ι), (⋂ i, s i) ⊆ s i := infi_le
 
 lemma Inter_subset_of_subset {s : ι → set α} {t : set α} (i : ι)
diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean
index b942af9af0ee7..693d323ee70b7 100644
--- a/src/linear_algebra/basis.lean
+++ b/src/linear_algebra/basis.lean
@@ -65,8 +65,10 @@ noncomputable theory
 open function set submodule
 open_locale classical big_operators
 
+universe u
+
 variables {ι : Type*} {ι' : Type*} {R : Type*} {K : Type*}
-          {M : Type*} {M' : Type*} {V : Type*} {V' : Type*}
+          {M : Type*} {M' : Type*} {V : Type u} {V' : Type*}
 
 section module
 variables {v : ι → M}
@@ -99,6 +101,13 @@ linear_independent_iff.trans
 λ hf l hl, finsupp.ext $ λ i, classical.by_contradiction $ λ hni, hni $ hf _ _ hl _ $
   finsupp.mem_support_iff.2 hni⟩
 
+theorem linear_dependent_iff : ¬ linear_independent R v ↔
+  ∃ s : finset ι, ∃ g : ι → R, s.sum (λ i, g i • v i) = 0 ∧ (∃ i ∈ s, g i ≠ 0) :=
+begin
+  rw linear_independent_iff',
+  simp only [exists_prop, classical.not_forall],
+end
+
 lemma linear_independent_empty_type (h : ¬ nonempty ι) : linear_independent R v :=
 begin
  rw [linear_independent_iff],
@@ -1056,6 +1065,27 @@ let ⟨b, hb₀, hx, hb₂, hb₃⟩ := exists_linear_independent hs (@subset_un
   @linear_independent.restrict_of_comp_subtype _ _ _ id _ _ _ _ hb₃,
   by simp; exact eq_top_iff.2 hb₂⟩
 
+lemma exists_sum_is_basis (hs : linear_independent K v) :
+  ∃ (ι' : Type u) (v' : ι' → V), is_basis K (sum.elim v v') :=
+begin
+  -- This is a hack: we jump through hoops to reuse `exists_subset_is_basis`.
+  let s := set.range v,
+  let e : ι ≃ s := equiv.set.range v (hs.injective zero_ne_one),
+  have : (λ x, x : s → V) = v ∘ e.symm := by { funext, dsimp, rw [equiv.set.apply_range_symm v], },
+  have : linear_independent K (λ x, x : s → V),
+  { rw this,
+    exact linear_independent.comp hs _ (e.symm.injective), },
+  obtain ⟨b, ss, is⟩ := exists_subset_is_basis this,
+  let e' : ι ⊕ (b \ s : set V) ≃ b :=
+  calc ι ⊕ (b \ s : set V) ≃ s ⊕ (b \ s : set V) : equiv.sum_congr e (equiv.refl _)
+                       ... ≃ b                   : equiv.set.sum_diff_subset ss,
+  refine ⟨(b \ s : set V), λ x, x.1, _⟩,
+  convert is_basis.comp is e' _,
+  { funext x,
+    cases x; simp; refl, },
+  { exact e'.bijective, },
+end
+
 variables (K V)
 lemma exists_is_basis : ∃b : set V, is_basis K (λ i, i : b → V) :=
 let ⟨b, _, hb⟩ := exists_subset_is_basis (linear_independent_empty K V : _) in ⟨b, hb⟩
diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean
index 31cdec0be3690..058c6ff585d95 100644
--- a/src/linear_algebra/dimension.lean
+++ b/src/linear_algebra/dimension.lean
@@ -23,10 +23,10 @@ import set_theory.ordinal
 
 noncomputable theory
 
-universes u u' u'' v v' w w'
+universes u u' u'' v' w w'
 
-variables {K : Type u} {V V₂ V₃ V₄ : Type v}
-variables {ι : Type w} {ι' : Type w'} {η : Type u''} {φ : η → Type u'}
+variables {K : Type u} {V V₂ V₃ V₄ : Type u'}
+variables {ι : Type w} {ι' : Type w'} {η : Type u''} {φ : η → Type*}
 -- TODO: relax these universe constraints
 
 open_locale classical big_operators
@@ -87,18 +87,18 @@ theorem mk_eq_mk_of_basis {v : ι → V} {v' : ι' → V}
   (hv : is_basis K v) (hv' : is_basis K v') :
   cardinal.lift.{w w'} (cardinal.mk ι) = cardinal.lift.{w' w} (cardinal.mk ι') :=
 begin
-  rw ←cardinal.lift_inj.{(max w w') v},
+  rw ←cardinal.lift_inj.{(max w w') u'},
   rw [cardinal.lift_lift, cardinal.lift_lift],
   apply le_antisymm,
-  { convert cardinal.lift_le.{v (max w w')}.2 (hv.le_span zero_ne_one hv'.2),
-    { rw cardinal.lift_max.{w v w'},
+  { convert cardinal.lift_le.{u' (max w w')}.2 (hv.le_span zero_ne_one hv'.2),
+    { rw cardinal.lift_max.{w u' w'},
       apply (cardinal.mk_range_eq_of_inj (hv.injective zero_ne_one)).symm, },
-    { rw cardinal.lift_max.{w' v w},
+    { rw cardinal.lift_max.{w' u' w},
       apply (cardinal.mk_range_eq_of_inj (hv'.injective zero_ne_one)).symm, }, },
-  { convert cardinal.lift_le.{v (max w w')}.2 (hv'.le_span zero_ne_one hv.2),
-    { rw cardinal.lift_max.{w' v w},
+  { convert cardinal.lift_le.{u' (max w w')}.2 (hv'.le_span zero_ne_one hv.2),
+    { rw cardinal.lift_max.{w' u' w},
       apply (cardinal.mk_range_eq_of_inj (hv'.injective zero_ne_one)).symm, },
-    { rw cardinal.lift_max.{w v w'},
+    { rw cardinal.lift_max.{w u' w'},
       apply (cardinal.mk_range_eq_of_inj (hv.injective zero_ne_one)).symm, }, }
 end
 
@@ -114,7 +114,7 @@ begin
 end
 
 theorem is_basis.mk_eq_dim {v : ι → V} (h : is_basis K v) :
-  cardinal.lift.{w v} (cardinal.mk ι) = cardinal.lift.{v w} (dim K V) :=
+  cardinal.lift.{w u'} (cardinal.mk ι) = cardinal.lift.{u' w} (dim K V) :=
 by rw [←h.mk_range_eq_dim, cardinal.mk_range_eq_of_inj (h.injective zero_ne_one)]
 
 variables [add_comm_group V₂] [vector_space K V₂]
@@ -147,6 +147,26 @@ lemma dim_span_set {s : set V} (hs : linear_independent K (λ x, x : s → V)) :
   dim K ↥(span K s) = cardinal.mk s :=
 by rw [← @set_of_mem_eq _ s, ← subtype.val_range]; exact dim_span hs
 
+lemma cardinal_le_dim_of_linear_independent
+  {ι : Type u'} {v : ι → V} (hv : linear_independent K v) :
+  (cardinal.mk ι) ≤ (dim.{u u'} K V) :=
+begin
+  obtain ⟨ι', v', is⟩ := exists_sum_is_basis hv,
+  simpa using le_trans
+    (cardinal.lift_mk_le.{u' u' u'}.2 ⟨@function.embedding.inl ι ι'⟩)
+    (le_of_eq is.mk_eq_dim),
+end
+
+lemma cardinal_le_dim_of_linear_independent'
+  {s : set V} (hs : linear_independent K (λ x, x : s → V)) :
+  cardinal.mk s ≤ dim K V :=
+begin
+  -- extend s to a basis
+  obtain ⟨b, ss, h⟩ := exists_subset_is_basis hs,
+  rw [←h.mk_range_eq_dim, range_coe_subtype],
+  apply cardinal.mk_le_of_injective (inclusion_injective ss),
+end
+
 lemma dim_span_le (s : set V) : dim K (span K s) ≤ cardinal.mk s :=
 begin
   classical,
@@ -316,8 +336,8 @@ lemma dim_fun {V η : Type u} [fintype η] [add_comm_group V] [vector_space K V]
 by rw [dim_pi, cardinal.sum_const, cardinal.fintype_card]
 
 lemma dim_fun_eq_lift_mul :
-  vector_space.dim K (η → V) = (fintype.card η : cardinal.{max u'' v}) *
-    cardinal.lift.{v u''} (vector_space.dim K V) :=
+  vector_space.dim K (η → V) = (fintype.card η : cardinal.{max u'' u'}) *
+    cardinal.lift.{u' u''} (vector_space.dim K V) :=
 by rw [dim_pi, cardinal.sum_const_eq_lift_mul, cardinal.fintype_card, cardinal.lift_nat_cast]
 
 lemma dim_fun' : vector_space.dim K (η → K) = fintype.card η :=
@@ -403,7 +423,7 @@ open vector_space
 
 /-- Version of linear_equiv.dim_eq without universe constraints. -/
 theorem linear_equiv.dim_eq_lift (f : V ≃ₗ[K] E) :
-  cardinal.lift.{v v'} (dim K V) = cardinal.lift.{v' v} (dim K E) :=
+  cardinal.lift.{u' v'} (dim K V) = cardinal.lift.{v' u'} (dim K E) :=
 begin
   cases exists_is_basis K V with b hb,
   rw [← cardinal.lift_inj.1 hb.mk_eq_dim, ← (f.is_basis hb).mk_eq_dim, cardinal.lift_mk],
diff --git a/src/logic/embedding.lean b/src/logic/embedding.lean
index 1c2d83950a4e8..a3d1697c9bece 100644
--- a/src/logic/embedding.lean
+++ b/src/logic/embedding.lean
@@ -150,6 +150,14 @@ def sum_congr {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α 
 @[simp] theorem sum_congr_apply_inr {α β γ δ}
   (e₁ : α ↪ β) (e₂ : γ ↪ δ) (b) : sum_congr e₁ e₂ (inr b) = inr (e₂ b) := rfl
 
+/-- The embedding of `α` into the sum `α ⊕ β`. -/
+def inl {α β : Type*} : α ↪ α ⊕ β :=
+⟨sum.inl, λ a b, sum.inl.inj⟩
+
+/-- The embedding of `β` into the sum `α ⊕ β`. -/
+def inr {α β : Type*} : β ↪ α ⊕ β :=
+⟨sum.inr, λ a b, sum.inr.inj⟩
+
 end sum
 
 section sigma