chore(linear_algebra/affine_space/combination): make k explicit in af…

…fine_combination (#18689)

The implicitness caused problems in elaboration. In Lean 3 it only amounts to long elaboration times, but in Lean 4 elaboration fails.

src/analysis/convex/between.lean

@@ -455,20 +455,14 @@ lemma sbtw.trans_wbtw_right_ne [no_zero_smul_divisors R V] {w x y z : P} (h₁ :
   (h₂ : wbtw R x y z) : w ≠ y :=
 h₁.wbtw.trans_right_ne h₂ h₁.left_ne
 
-/- Calls to `affine_combination` are slow to elaborate (generally, not just for this lemma), and
-without the use of `@finset.affine_combination R V _ _ _ _ _ _` for at least three of the six
-calls in this lemma statement, elaboration of the statement times out (even if the proof is
-replaced by `sorry`). -/
 lemma sbtw.affine_combination_of_mem_affine_span_pair [no_zero_divisors R]
   [no_zero_smul_divisors R V] {ι : Type*} {p : ι → P} (ha : affine_independent R p)
   {w w₁ w₂ : ι → R} {s : finset ι} (hw : ∑ i in s, w i = 1) (hw₁ : ∑ i in s, w₁ i = 1)
   (hw₂ : ∑ i in s, w₂ i = 1)
-  (h : s.affine_combination p w ∈
-    line[R, s.affine_combination p w₁, s.affine_combination p w₂]) {i : ι} (his : i ∈ s)
-  (hs : sbtw R (w₁ i) (w i) (w₂ i)) :
-  sbtw R (@finset.affine_combination R V _ _ _ _ _ _ s p w₁)
-    (@finset.affine_combination R V _ _ _ _ _ _ s p w)
-    (@finset.affine_combination R V _ _ _ _ _ _ s p w₂) :=
+  (h : s.affine_combination R p w ∈
+    line[R, s.affine_combination R p w₁, s.affine_combination R p w₂])
+  {i : ι} (his : i ∈ s) (hs : sbtw R (w₁ i) (w i) (w₂ i)) :
+  sbtw R (s.affine_combination R p w₁) (s.affine_combination R p w) (s.affine_combination R p w₂) :=
 begin
   rw affine_combination_mem_affine_span_pair ha hw hw₁ hw₂ at h,
   rcases h with ⟨r, hr⟩,

src/analysis/convex/combination.lean

@@ -223,7 +223,7 @@ t.center_mass_mem_convex_hull hw₀ hws (λ i, mem_coe.2)
 
 lemma affine_combination_eq_center_mass {ι : Type*} {t : finset ι} {p : ι → E} {w : ι → R}
   (hw₂ : ∑ i in t, w i = 1) :
-  affine_combination t p w = center_mass t w p :=
+  t.affine_combination R p w = center_mass t w p :=
 begin
   rw [affine_combination_eq_weighted_vsub_of_point_vadd_of_sum_eq_one _ w _ hw₂ (0 : E),
     finset.weighted_vsub_of_point_apply, vadd_eq_add, add_zero, t.center_mass_eq_of_sum_1 _ hw₂],
@@ -232,7 +232,7 @@ end
 
 lemma affine_combination_mem_convex_hull
   {s : finset ι} {v : ι → E} {w : ι → R} (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : s.sum w = 1) :
-  s.affine_combination v w ∈ convex_hull R (range v) :=
+  s.affine_combination R v w ∈ convex_hull R (range v) :=
 begin
   rw affine_combination_eq_center_mass hw₁,
   apply s.center_mass_mem_convex_hull hw₀,
@@ -258,7 +258,7 @@ end
 
 lemma convex_hull_range_eq_exists_affine_combination (v : ι → E) :
   convex_hull R (range v) = { x | ∃ (s : finset ι) (w : ι → R)
-    (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : s.sum w = 1), s.affine_combination v w = x } :=
+    (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : s.sum w = 1), s.affine_combination R v w = x } :=
 begin
   refine subset.antisymm (convex_hull_min _ _) _,
   { intros x hx,

src/geometry/euclidean/basic.lean

@@ -86,11 +86,11 @@ in terms of the pairwise distances between the points in that
 combination. -/
 lemma dist_affine_combination {ι : Type*} {s : finset ι} {w₁ w₂ : ι → ℝ} (p : ι → P)
     (h₁ : ∑ i in s, w₁ i = 1) (h₂ : ∑ i in s, w₂ i = 1) :
-  by have a₁ := s.affine_combination p w₁; have a₂ := s.affine_combination p w₂; exact
+  by have a₁ := s.affine_combination ℝ p w₁; have a₂ := s.affine_combination ℝ p w₂; exact
   dist a₁ a₂ * dist a₁ a₂ = (-∑ i₁ in s, ∑ i₂ in s,
       (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2 :=
 begin
-  rw [dist_eq_norm_vsub V (s.affine_combination p w₁) (s.affine_combination p w₂),
+  rw [dist_eq_norm_vsub V (s.affine_combination ℝ p w₁) (s.affine_combination ℝ p w₂),
       ←@inner_self_eq_norm_mul_norm ℝ, finset.affine_combination_vsub],
   have h : ∑ i in s, (w₁ - w₂) i = 0,
   { simp_rw [pi.sub_apply, finset.sum_sub_distrib, h₁, h₂, sub_self] },

src/geometry/euclidean/circumcenter.lean

@@ -583,7 +583,7 @@ include V
 lemma point_eq_affine_combination_of_points_with_circumcenter {n : ℕ} (s : simplex ℝ P n)
   (i : fin (n + 1)) :
   s.points i =
-    (univ : finset (points_with_circumcenter_index n)).affine_combination
+    (univ : finset (points_with_circumcenter_index n)).affine_combination ℝ
       s.points_with_circumcenter (point_weights_with_circumcenter i) :=
 begin
   rw ←points_with_circumcenter_point,
@@ -627,7 +627,7 @@ include V
 lemma centroid_eq_affine_combination_of_points_with_circumcenter {n : ℕ} (s : simplex ℝ P n)
   (fs : finset (fin (n + 1))) :
   fs.centroid ℝ s.points =
-    (univ : finset (points_with_circumcenter_index n)).affine_combination
+    (univ : finset (points_with_circumcenter_index n)).affine_combination ℝ
       s.points_with_circumcenter (centroid_weights_with_circumcenter fs) :=
 begin
   simp_rw [centroid_def, affine_combination_apply,
@@ -666,7 +666,7 @@ include V
 `points_with_circumcenter`. -/
 lemma circumcenter_eq_affine_combination_of_points_with_circumcenter {n : ℕ}
   (s : simplex ℝ P n) :
-  s.circumcenter = (univ : finset (points_with_circumcenter_index n)).affine_combination
+  s.circumcenter = (univ : finset (points_with_circumcenter_index n)).affine_combination ℝ
     s.points_with_circumcenter (circumcenter_weights_with_circumcenter n) :=
 begin
   rw ←points_with_circumcenter_eq_circumcenter,
@@ -702,7 +702,7 @@ terms of `points_with_circumcenter`. -/
 lemma reflection_circumcenter_eq_affine_combination_of_points_with_circumcenter {n : ℕ}
   (s : simplex ℝ P n) {i₁ i₂ : fin (n + 1)} (h : i₁ ≠ i₂) :
   reflection (affine_span ℝ (s.points '' {i₁, i₂})) s.circumcenter =
-    (univ : finset (points_with_circumcenter_index n)).affine_combination
+    (univ : finset (points_with_circumcenter_index n)).affine_combination ℝ
       s.points_with_circumcenter (reflection_circumcenter_weights_with_circumcenter i₁ i₂) :=
 begin
   have hc : card ({i₁, i₂} : finset (fin (n + 1))) = 2,

src/geometry/euclidean/monge_point.lean

@@ -126,7 +126,7 @@ include V
 `points_with_circumcenter`. -/
 lemma monge_point_eq_affine_combination_of_points_with_circumcenter {n : ℕ}
   (s : simplex ℝ P (n + 2)) :
-  s.monge_point = (univ : finset (points_with_circumcenter_index (n + 2))).affine_combination
+  s.monge_point = (univ : finset (points_with_circumcenter_index (n + 2))).affine_combination ℝ
     s.points_with_circumcenter (monge_point_weights_with_circumcenter n) :=
 begin
   rw [monge_point_eq_smul_vsub_vadd_circumcenter,

src/linear_algebra/affine_space/basis.lean

@@ -145,15 +145,15 @@ lemma coord_apply [decidable_eq ι] (i j : ι) : b.coord i (b j) = if i = j then
 by cases eq_or_ne i j; simp [h]
 
 @[simp] lemma coord_apply_combination_of_mem (hi : i ∈ s) {w : ι → k} (hw : s.sum w = 1) :
-  b.coord i (s.affine_combination b w) = w i :=
+  b.coord i (s.affine_combination k b w) = w i :=
 begin
   classical,
   simp only [coord_apply, hi, finset.affine_combination_eq_linear_combination, if_true, mul_boole,
     hw, function.comp_app, smul_eq_mul, s.sum_ite_eq, s.map_affine_combination b w hw],
 end
 
 @[simp] lemma coord_apply_combination_of_not_mem (hi : i ∉ s) {w : ι → k} (hw : s.sum w = 1) :
-  b.coord i (s.affine_combination b w) = 0 :=
+  b.coord i (s.affine_combination k b w) = 0 :=
 begin
   classical,
   simp only [coord_apply, hi, finset.affine_combination_eq_linear_combination, if_false, mul_boole,
@@ -171,7 +171,7 @@ begin
 end
 
 @[simp] lemma affine_combination_coord_eq_self [fintype ι] (q : P) :
-  finset.univ.affine_combination b (λ i, b.coord i q) = q :=
+  finset.univ.affine_combination k b (λ i, b.coord i q) = q :=
 begin
   have hq : q ∈ affine_span k (range b), { rw b.tot, exact affine_subspace.mem_top k V q, },
   obtain ⟨w, hw, rfl⟩ := eq_affine_combination_of_mem_affine_span_of_fintype hq,
@@ -208,7 +208,7 @@ begin
   let s : finset ι := {i},
   have hi : i ∈ s, { simp, },
   have hw : s.sum (function.const ι (1 : k)) = 1, { simp, },
-  have hq : q = s.affine_combination b (function.const ι (1 : k)), { simp, },
+  have hq : q = s.affine_combination k b (function.const ι (1 : k)), { simp, },
   rw [pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw],
 end
 
@@ -223,7 +223,7 @@ begin
   have hj : j ∈ s, { simp, },
   let w : ι → k := λ j', if j' = i then x else 1-x,
   have hw : s.sum w = 1, { simp [hij, finset.sum_ite, finset.filter_insert, finset.filter_eq'], },
-  use s.affine_combination b w,
+  use s.affine_combination k b w,
   simp [b.coord_apply_combination_of_mem hi hw],
 end