refactor(linear_algebra,analysis/normed_space): use finite, review API, golf (#17320)

* replace `fintype_of_fin_dim_affine_independent` with `finite_of_fin_dim_affine_independent`;
* rename old `finite_of_fin_dim_affine_independent` to `finite_set_of_fin_dim_affine_independent`, generalize;
* define `affine_basis.comp_equiv`;
* add `affine_basis.finite`, `affine_basis.finite_set`, `affine_basis.coord_apply_centroid`, `affine_basis.card_eq_finrank_add_one`
* use more precise statement in `exists_affine_basis`, add `exists_affine_subbasis`;
* rename `interior_convex_hull_aff_basis` to `affine_basis.interior_convex_hull`;
* rename `exists_subset_affine_independent_span_eq_top_of_open` to `is_open.exists_between_affine_independent_span_eq_top`, golf;
* add `is_open.exists_subset_affine_independent_span_eq_top`, `is_open.affine_span_eq_top`, `affine_span_eq_top_of_nonempty_interior`, and `affine_basis.centroid_mem_interior_convex_hull`;
* rename `interior_convex_hull_nonempty_iff_aff_span_eq_top` to `interior_convex_hull_nonempty_iff_affine_span_eq_top`

Author: urkud

src/analysis/normed_space/add_torsor_bases.lean

@@ -19,9 +19,9 @@ This file contains results about bases in normed affine spaces.
 
  * `continuous_barycentric_coord`
  * `is_open_map_barycentric_coord`
- * `interior_convex_hull_aff_basis`
+ * `affine_basis.interior_convex_hull`
  * `exists_subset_affine_independent_span_eq_top_of_open`
- * `interior_convex_hull_nonempty_iff_aff_span_eq_top`
+ * `interior_convex_hull_nonempty_iff_affine_span_eq_top`
 -/
 
 section barycentric
@@ -54,9 +54,9 @@ to this basis.
 
 TODO Restate this result for affine spaces (instead of vector spaces) once the definition of
 convexity is generalised to this setting. -/
-lemma interior_convex_hull_aff_basis {ι E : Type*} [finite ι] [normed_add_comm_group E]
+lemma affine_basis.interior_convex_hull {ι E : Type*} [finite ι] [normed_add_comm_group E]
   [normed_space ℝ E] (b : affine_basis ι ℝ E) :
-  interior (convex_hull ℝ (range b.points)) = { x | ∀ i, 0 < b.coord i x } :=
+  interior (convex_hull ℝ (range b.points)) = {x | ∀ i, 0 < b.coord i x} :=
 begin
   casesI subsingleton_or_nontrivial ι,
   { -- The zero-dimensional case.
@@ -66,7 +66,7 @@ begin
   { -- The positive-dimensional case.
     haveI : finite_dimensional ℝ E := b.finite_dimensional,
     have : convex_hull ℝ (range b.points) = ⋂ i, (b.coord i)⁻¹' Ici 0,
-    { rw convex_hull_affine_basis_eq_nonneg_barycentric b, ext, simp, },
+    { rw [convex_hull_affine_basis_eq_nonneg_barycentric b, set_of_forall], refl },
     ext,
     simp only [this, interior_Inter, ← is_open_map.preimage_interior_eq_interior_preimage
       (is_open_map_barycentric_coord b _) (continuous_barycentric_coord b _),
@@ -81,77 +81,77 @@ open affine_map
 
 /-- Given a set `s` of affine-independent points belonging to an open set `u`, we may extend `s` to
 an affine basis, all of whose elements belong to `u`. -/
-lemma exists_subset_affine_independent_span_eq_top_of_open {s u : set P} (hu : is_open u)
+lemma is_open.exists_between_affine_independent_span_eq_top {s u : set P} (hu : is_open u)
   (hsu : s ⊆ u) (hne : s.nonempty) (h : affine_independent ℝ (coe : s → P)) :
   ∃ t : set P, s ⊆ t ∧ t ⊆ u ∧ affine_independent ℝ (coe : t → P) ∧ affine_span ℝ t = ⊤ :=
 begin
   obtain ⟨q, hq⟩ := hne,
-  obtain ⟨ε, hε, hεu⟩ := metric.is_open_iff.mp hu q (hsu hq),
+  obtain ⟨ε, ε0, hεu⟩ := metric.nhds_basis_closed_ball.mem_iff.1 (hu.mem_nhds $ hsu hq),
   obtain ⟨t, ht₁, ht₂, ht₃⟩ := exists_subset_affine_independent_affine_span_eq_top h,
-  let f : P → P := λ y, line_map q y (ε / 2 / (dist y q)),
+  let f : P → P := λ y, line_map q y (ε / dist y q),
   have hf : ∀ y, f y ∈ u,
-  { intros y,
-    apply hεu,
-    simp only [metric.mem_ball, f, line_map_apply, dist_vadd_left, norm_smul, real.norm_eq_abs,
-      dist_eq_norm_vsub V y q],
-    cases eq_or_ne (∥y -ᵥ q∥) 0 with hyq hyq, { rwa [hyq, mul_zero], },
-    rw [← norm_pos_iff, norm_norm] at hyq,
-    calc abs (ε / 2 / ∥y -ᵥ q∥) * ∥y -ᵥ q∥
-          = ε / 2 / ∥y -ᵥ q∥ * ∥y -ᵥ q∥ : by rw [abs_div, abs_of_pos (half_pos hε), abs_of_pos hyq]
-      ... = ε / 2 : div_mul_cancel _ (ne_of_gt hyq)
-      ... < ε : half_lt_self hε, },
-  have hεyq : ∀ (y ∉ s), ε / 2 / dist y q ≠ 0,
-  { simp only [ne.def, div_eq_zero_iff, or_false, dist_eq_zero, bit0_eq_zero, one_ne_zero,
-      not_or_distrib, ne_of_gt hε, true_and, not_false_iff],
-    exact λ y h1 h2, h1 (h2.symm ▸ hq) },
+  { refine λ y, hεu _,
+    simp only [f],
+    rw [metric.mem_closed_ball, line_map_apply, dist_vadd_left, norm_smul, real.norm_eq_abs,
+      dist_eq_norm_vsub V y q, abs_div, abs_of_pos ε0, abs_of_nonneg (norm_nonneg _), div_mul_comm],
+    exact mul_le_of_le_one_left ε0.le (div_self_le_one _) },
+  have hεyq : ∀ y ∉ s, ε / dist y q ≠ 0,
+    from λ y hy, div_ne_zero ε0.ne' (dist_ne_zero.2 (ne_of_mem_of_not_mem hq hy).symm),
   classical,
   let w : t → ℝˣ := λ p, if hp : (p : P) ∈ s then 1 else units.mk0 _ (hεyq ↑p hp),
   refine ⟨set.range (λ (p : t), line_map q p (w p : ℝ)), _, _, _, _⟩,
   { intros p hp, use ⟨p, ht₁ hp⟩, simp [w, hp], },
-  { intros y hy,
-    simp only [set.mem_range, set_coe.exists, subtype.coe_mk] at hy,
-    obtain ⟨p, hp, hyq⟩ := hy,
-    by_cases hps : p ∈ s;
-    simp only [w, hps, line_map_apply_one, units.coe_mk0, dif_neg, dif_pos, not_false_iff,
-      units.coe_one, subtype.coe_mk] at hyq;
-    rw ← hyq;
-    [exact hsu hps, exact hf p], },
+  { rintros y ⟨⟨p, hp⟩, rfl⟩,
+    by_cases hps : p ∈ s; simp only [w, hps, line_map_apply_one, units.coe_mk0, dif_neg, dif_pos,
+      not_false_iff, units.coe_one, subtype.coe_mk];
+      [exact hsu hps, exact hf p], },
   { exact (ht₂.units_line_map ⟨q, ht₁ hq⟩ w).range, },
   { rw [affine_span_eq_affine_span_line_map_units (ht₁ hq) w, ht₃], },
 end
 
-lemma interior_convex_hull_nonempty_iff_aff_span_eq_top [finite_dimensional ℝ V] {s : set V} :
+lemma is_open.exists_subset_affine_independent_span_eq_top {u : set P} (hu : is_open u)
+  (hne : u.nonempty) :
+  ∃ s ⊆ u, affine_independent ℝ (coe : s → P) ∧ affine_span ℝ s = ⊤ :=
+begin
+  rcases hne with ⟨x, hx⟩,
+  rcases hu.exists_between_affine_independent_span_eq_top (singleton_subset_iff.mpr hx)
+    (singleton_nonempty _) (affine_independent_of_subsingleton _ _) with ⟨s, -, hsu, hs⟩,
+  exact ⟨s, hsu, hs⟩
+end
+
+/-- The affine span of a nonempty open set is `⊤`. -/
+lemma is_open.affine_span_eq_top {u : set P} (hu : is_open u) (hne : u.nonempty) :
+  affine_span ℝ u = ⊤ :=
+let ⟨s, hsu, hs, hs'⟩ := hu.exists_subset_affine_independent_span_eq_top hne
+in top_unique $ hs' ▸ affine_span_mono _ hsu
+
+lemma affine_span_eq_top_of_nonempty_interior {s : set V}
+  (hs : (interior $ convex_hull ℝ s).nonempty) :
+  affine_span ℝ s = ⊤ :=
+top_unique $ is_open_interior.affine_span_eq_top hs ▸
+  (affine_span_mono _ interior_subset).trans_eq (affine_span_convex_hull _)
+
+lemma affine_basis.centroid_mem_interior_convex_hull {ι} [fintype ι] (b : affine_basis ι ℝ V) :
+  finset.univ.centroid ℝ b.points ∈ interior (convex_hull ℝ (range b.points)) :=
+begin
+  haveI := b.nonempty,
+  simp only [b.interior_convex_hull, mem_set_of_eq, b.coord_apply_centroid (finset.mem_univ _),
+    inv_pos, nat.cast_pos, finset.card_pos, finset.univ_nonempty, forall_true_iff]
+end
+
+lemma interior_convex_hull_nonempty_iff_affine_span_eq_top [finite_dimensional ℝ V] {s : set V} :
   (interior (convex_hull ℝ s)).nonempty ↔ affine_span ℝ s = ⊤ :=
 begin
-  split,
-  { rintros ⟨x, hx⟩,
-    obtain ⟨u, hu₁, hu₂, hu₃⟩ := mem_interior.mp hx,
-    let t : set V := {x},
-    obtain ⟨b, hb₁, hb₂, hb₃, hb₄⟩ := exists_subset_affine_independent_span_eq_top_of_open hu₂
-      (singleton_subset_iff.mpr hu₃) (singleton_nonempty x)
-      (affine_independent_of_subsingleton ℝ (coe : t → V)),
-    rw [eq_top_iff, ← hb₄, ← affine_span_convex_hull s],
-    mono,
-    exact hb₂.trans hu₁, },
-  { intros h,
-    obtain ⟨t, hts, h_tot, h_ind⟩ := exists_affine_independent ℝ V s,
-    suffices : (interior (convex_hull ℝ (range (coe : t → V)))).nonempty,
-    { rw [subtype.range_coe_subtype, set_of_mem_eq] at this,
-      apply nonempty.mono _ this,
-      mono* },
-    haveI : fintype t := fintype_of_fin_dim_affine_independent ℝ h_ind,
-    use finset.centroid ℝ (finset.univ : finset t) (coe : t → V),
-    rw [h, ← @set_of_mem_eq V t, ← subtype.range_coe_subtype] at h_tot,
-    let b : affine_basis t ℝ V := ⟨coe, h_ind, h_tot⟩,
-    rw interior_convex_hull_aff_basis b,
-    have htne : (finset.univ : finset t).nonempty,
-    { simpa [finset.univ_nonempty_iff] using
-        affine_subspace.nonempty_of_affine_span_eq_top ℝ V V h_tot, },
-    simp [finset.centroid_def, b.coord_apply_combination_of_mem (finset.mem_univ _)
-      (finset.sum_centroid_weights_eq_one_of_nonempty ℝ (finset.univ : finset t) htne),
-      finset.centroid_weights_apply, nat.cast_pos, inv_pos, finset.card_pos.mpr htne], },
+  refine ⟨affine_span_eq_top_of_nonempty_interior, λ h, _⟩,
+  obtain ⟨t, hts, b, hb⟩ := affine_basis.exists_affine_subbasis h,
+  suffices : (interior (convex_hull ℝ (range b.points))).nonempty,
+  { rw [hb, subtype.range_coe_subtype, set_of_mem_eq] at this,
+    refine this.mono _,
+    mono* },
+  lift t to finset V using b.finite_set,
+  exact ⟨_, b.centroid_mem_interior_convex_hull⟩
 end
 
 lemma convex.interior_nonempty_iff_affine_span_eq_top [finite_dimensional ℝ V] {s : set V}
   (hs : convex ℝ s) : (interior s).nonempty ↔ affine_span ℝ s = ⊤ :=
-by rw [← interior_convex_hull_nonempty_iff_aff_span_eq_top, hs.convex_hull_eq]
+by rw [← interior_convex_hull_nonempty_iff_affine_span_eq_top, hs.convex_hull_eq]

src/analysis/normed_space/finite_dimension.lean

@@ -209,7 +209,7 @@ end
 lemma linear_map.exists_antilipschitz_with [finite_dimensional 𝕜 E] (f : E →ₗ[𝕜] F)
   (hf : f.ker = ⊥) : ∃ K > 0, antilipschitz_with K f :=
 begin
-  cases subsingleton_or_nontrivial E; resetI,
+  casesI subsingleton_or_nontrivial E,
   { exact ⟨1, zero_lt_one, antilipschitz_with.of_subsingleton⟩ },
   { rw linear_map.ker_eq_bot at hf,
     let e : E ≃L[𝕜] f.range := (linear_equiv.of_injective f hf).to_continuous_linear_equiv,

src/data/set/finite.lean

@@ -485,6 +485,9 @@ alias finite_univ_iff ↔ _root_.finite.of_finite_univ _
 theorem finite.union {s t : set α} (hs : s.finite) (ht : t.finite) : (s ∪ t).finite :=
 by { casesI hs, casesI ht, apply to_finite }
 
+theorem finite.finite_of_compl {s : set α} (hs : s.finite) (hsc : sᶜ.finite) : finite α :=
+by { rw [← finite_univ_iff, ← union_compl_self s], exact hs.union hsc }
+
 lemma finite.sup {s t : set α} : s.finite → t.finite → (s ⊔ t).finite := finite.union
 
 theorem finite.sep {s : set α} (hs : s.finite) (p : α → Prop) : {a ∈ s | p a}.finite :=

src/linear_algebra/affine_space/basis.lean

@@ -72,6 +72,10 @@ protected lemma nonempty : nonempty ι :=
 not_is_empty_iff.mp $ λ hι,
   by simpa only [@range_eq_empty _ _ hι, affine_subspace.span_empty, bot_ne_top] using b.tot
 
+/-- Composition of an affine basis and an equivalence of index types. -/
+def comp_equiv {ι'} (e : ι' ≃ ι) : affine_basis ι' k P :=
+⟨b.points ∘ e, b.ind.comp_embedding e.to_embedding, by { rw [e.surjective.range_comp], exact b.3 }⟩
+
 /-- Given an affine basis for an affine space `P`, if we single out one member of the family, we
 obtain a linear basis for the model space `V`.
 
@@ -371,29 +375,49 @@ include V
 protected lemma finite_dimensional [finite ι] (b : affine_basis ι k P) : finite_dimensional k V :=
 let ⟨i⟩ := b.nonempty in finite_dimensional.of_fintype_basis (b.basis_of i)
 
-variables (k V P)
+protected lemma finite [finite_dimensional k V] (b : affine_basis ι k P) : finite ι :=
+finite_of_fin_dim_affine_independent k b.ind
+
+protected lemma finite_set [finite_dimensional k V] {s : set ι} (b : affine_basis s k P) :
+  s.finite :=
+finite_set_of_fin_dim_affine_independent k b.ind
+
+@[simp] lemma coord_apply_centroid [char_zero k] (b : affine_basis ι k P) {s : finset ι} {i : ι}
+  (hi : i ∈ s) :
+  b.coord i (s.centroid k b.points) = (s.card : k) ⁻¹ :=
+by rw [finset.centroid, b.coord_apply_combination_of_mem hi
+  (s.sum_centroid_weights_eq_one_of_nonempty _ ⟨i, hi⟩), finset.centroid_weights]
+
+lemma card_eq_finrank_add_one [fintype ι] (b : affine_basis ι k P) :
+  fintype.card ι = finite_dimensional.finrank k V + 1 :=
+begin
+  haveI := b.finite_dimensional,
+  exact b.ind.affine_span_eq_top_iff_card_eq_finrank_add_one.mp b.tot
+end
 
-lemma exists_affine_basis : ∃ (s : set P), nonempty (affine_basis ↥s k P) :=
+lemma exists_affine_subbasis {t : set P} (ht : affine_span k t = ⊤) :
+  ∃ (s ⊆ t) (b : affine_basis ↥s k P), b.points = coe :=
 begin
-  obtain ⟨s, -, h_tot, h_ind⟩ := exists_affine_independent k V (set.univ : set P),
-  refine ⟨s, ⟨⟨(coe : s → P), h_ind, _⟩⟩⟩,
-  rw [subtype.range_coe, h_tot, affine_subspace.span_univ],
+  obtain ⟨s, hst, h_tot, h_ind⟩ := exists_affine_independent k V t,
+  refine ⟨s, hst, ⟨coe, h_ind, _⟩, rfl⟩,
+  rw [subtype.range_coe, h_tot, ht]
 end
 
+variables (k V P)
+
+lemma exists_affine_basis : ∃ (s : set P) (b : affine_basis ↥s k P), b.points = coe :=
+let ⟨s, _, hs⟩ := exists_affine_subbasis (affine_subspace.span_univ k V P) in ⟨s, hs⟩
+
 variables {k V P}
 
-lemma exists_affine_basis_of_finite_dimensional {ι : Type*} [fintype ι] [finite_dimensional k V]
+lemma exists_affine_basis_of_finite_dimensional [fintype ι] [finite_dimensional k V]
   (h : fintype.card ι = finite_dimensional.finrank k V + 1) :
   nonempty (affine_basis ι k P) :=
 begin
-  obtain ⟨s, ⟨⟨incl, h_ind, h_tot⟩⟩⟩ := affine_basis.exists_affine_basis k V P,
-  haveI : fintype s := fintype_of_fin_dim_affine_independent k h_ind,
-  have hs : fintype.card ι = fintype.card s,
-  { rw h, exact (h_ind.affine_span_eq_top_iff_card_eq_finrank_add_one.mp h_tot).symm, },
-  rw ← affine_independent_equiv (fintype.equiv_of_card_eq hs) at h_ind,
-  refine ⟨⟨_, h_ind, _⟩⟩,
-  rw range_comp,
-  simp [h_tot],
+  obtain ⟨s, b, hb⟩ := affine_basis.exists_affine_basis k V P,
+  lift s to finset P using b.finite_set,
+  refine ⟨b.comp_equiv $ fintype.equiv_of_card_eq _⟩,
+  rw [h, ← b.card_eq_finrank_add_one]
 end
 
 end division_ring

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -68,21 +68,22 @@ instance finite_dimensional_direction_affine_span_image_of_finite [_root_.finite
 finite_dimensional_direction_affine_span_of_finite k (set.to_finite _)
 
 /-- An affine-independent family of points in a finite-dimensional affine space is finite. -/
-noncomputable def fintype_of_fin_dim_affine_independent [finite_dimensional k V]
-  {p : ι → P} (hi : affine_independent k p) : fintype ι :=
-by classical; exact if hι : is_empty ι then (@fintype.of_is_empty _ hι) else
+lemma finite_of_fin_dim_affine_independent [finite_dimensional k V] {p : ι → P}
+  (hi : affine_independent k p) : _root_.finite ι :=
 begin
-  let q := (not_is_empty_iff.mp hι).some,
-  rw affine_independent_iff_linear_independent_vsub k p q at hi,
+  nontriviality ι, inhabit ι,
+  rw affine_independent_iff_linear_independent_vsub k p default at hi,
   letI : is_noetherian k V := is_noetherian.iff_fg.2 infer_instance,
-  exact fintype_of_fintype_ne _ (@fintype.of_finite _ hi.finite_of_is_noetherian),
+  exact (set.finite_singleton default).finite_of_compl
+    (set.finite_coe_iff.1 hi.finite_of_is_noetherian)
 end
 
 /-- An affine-independent subset of a finite-dimensional affine space is finite. -/
-lemma finite_of_fin_dim_affine_independent [finite_dimensional k V]
-  {s : set P} (hi : affine_independent k (coe : s → P)) : s.finite :=
-⟨fintype_of_fin_dim_affine_independent k hi⟩
+lemma finite_set_of_fin_dim_affine_independent [finite_dimensional k V] {s : set ι} {f : s → P}
+  (hi : affine_independent k f) : s.finite :=
+@set.to_finite _ s (finite_of_fin_dim_affine_independent k hi)
 
+open_locale classical
 variables {k}
 
 /-- The `vector_span` of a finite subset of an affinely independent