feat(linear_algebra/affine_space/combination): vsub distributivity le…

…mmas

Add lemmas about weighted sums of `-ᵥ` expressions in terms of
`weighted_vsub_of_point`, `weighted_vsub` and `affine_combination`,
with special cases where the points on one side of the subtractions
are constant, and lemmas about those three functions for constant
points used to prove those special cases.

These were suggested by one of the lemmas in #10632; the lemma
`affine_basis.vsub_eq_coord_smul_sum` is a very specific case, but
showed up that these distributivity lemmas were missing (and should
follow immediately from
`sum_smul_vsub_const_eq_vsub_affine_combination` in this PR).

src/linear_algebra/affine_space/combination.lean

@@ -67,6 +67,11 @@ def weighted_vsub_of_point (p : ι → P) (b : P) : (ι → k) →ₗ[k] V :=
   s.weighted_vsub_of_point p b w = ∑ i in s, w i • (p i -ᵥ b) :=
 by simp [weighted_vsub_of_point, linear_map.sum_apply]
 
+/-- The value of `weighted_vsub_of_point`, where the given points are equal. -/
+@[simp] lemma weighted_vsub_of_point_apply_const (w : ι → k) (p : P) (b : P) :
+  s.weighted_vsub_of_point (λ _, p) b w = (∑ i in s, w i) • (p -ᵥ b) :=
+by rw [weighted_vsub_of_point_apply, sum_smul]
+
 /-- Given a family of points, if we use a member of the family as a base point, the
 `weighted_vsub_of_point` does not depend on the value of the weights at this point. -/
 lemma weighted_vsub_of_point_eq_of_weights_eq
@@ -155,6 +160,25 @@ begin
   exact finset.sum_map _ _ _
 end
 
+/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two
+`weighted_vsub_of_point` expressions. -/
+lemma sum_smul_vsub_eq_weighted_vsub_of_point_sub (w : ι → k) (p₁ p₂ : ι → P) (b : P) :
+  ∑ i in s, w i • (p₁ i -ᵥ p₂ i) =
+    s.weighted_vsub_of_point p₁ b w - s.weighted_vsub_of_point p₂ b w :=
+by simp_rw [weighted_vsub_of_point_apply, ←sum_sub_distrib, ←smul_sub, vsub_sub_vsub_cancel_right]
+
+/-- A weighted sum of pairwise subtractions, where the point on the right is constant,
+expressed as a subtraction involving a `weighted_vsub_of_point` expression. -/
+lemma sum_smul_vsub_const_eq_weighted_vsub_of_point_sub (w : ι → k) (p₁ : ι → P) (p₂ b : P) :
+  ∑ i in s, w i • (p₁ i -ᵥ p₂) = s.weighted_vsub_of_point p₁ b w - (∑ i in s, w i) • (p₂ -ᵥ b) :=
+by rw [sum_smul_vsub_eq_weighted_vsub_of_point_sub, weighted_vsub_of_point_apply_const]
+
+/-- A weighted sum of pairwise subtractions, where the point on the left is constant,
+expressed as a subtraction involving a `weighted_vsub_of_point` expression. -/
+lemma sum_smul_const_vsub_eq_sub_weighted_vsub_of_point (w : ι → k) (p₂ : ι → P) (p₁ b : P) :
+  ∑ i in s, w i • (p₁ -ᵥ p₂ i) = (∑ i in s, w i) • (p₁ -ᵥ b) - s.weighted_vsub_of_point p₂ b w :=
+by rw [sum_smul_vsub_eq_weighted_vsub_of_point_sub, weighted_vsub_of_point_apply_const]
+
 /-- A weighted sum of the results of subtracting a default base point
 from the given points, as a linear map on the weights.  This is
 intended to be used when the sum of the weights is 0; that condition
@@ -178,6 +202,12 @@ lemma weighted_vsub_eq_weighted_vsub_of_point_of_sum_eq_zero (w : ι → k) (p :
     (h : ∑ i in s, w i = 0) (b : P) : s.weighted_vsub p w = s.weighted_vsub_of_point p b w :=
 s.weighted_vsub_of_point_eq_of_sum_eq_zero w p h _ _
 
+/-- The value of `weighted_vsub`, where the given points are equal and the sum of the weights
+is 0. -/
+@[simp] lemma weighted_vsub_apply_const (w : ι → k) (p : P) (h : ∑ i in s, w i = 0) :
+  s.weighted_vsub (λ _, p) w = 0 :=
+by rw [weighted_vsub, weighted_vsub_of_point_apply_const, h, zero_smul]
+
 /-- The `weighted_vsub` for an empty set is 0. -/
 @[simp] lemma weighted_vsub_empty (w : ι → k) (p : ι → P) :
   (∅ : finset ι).weighted_vsub p w = (0:V) :=
@@ -196,6 +226,26 @@ lemma weighted_vsub_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) :
   (s₂.map e).weighted_vsub p w = s₂.weighted_vsub (p ∘ e) (w ∘ e) :=
 s₂.weighted_vsub_of_point_map _ _ _ _
 
+/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two `weighted_vsub`
+expressions. -/
+lemma sum_smul_vsub_eq_weighted_vsub_sub (w : ι → k) (p₁ p₂ : ι → P) :
+  ∑ i in s, w i • (p₁ i -ᵥ p₂ i) = s.weighted_vsub p₁ w - s.weighted_vsub p₂ w :=
+s.sum_smul_vsub_eq_weighted_vsub_of_point_sub _ _ _ _
+
+/-- A weighted sum of pairwise subtractions, where the point on the right is constant and the
+sum of the weights is 0. -/
+lemma sum_smul_vsub_const_eq_weighted_vsub (w : ι → k) (p₁ : ι → P) (p₂ : P)
+  (h : ∑ i in s, w i = 0) :
+  ∑ i in s, w i • (p₁ i -ᵥ p₂) = s.weighted_vsub p₁ w :=
+by rw [sum_smul_vsub_eq_weighted_vsub_sub, s.weighted_vsub_apply_const _ _ h, sub_zero]
+
+/-- A weighted sum of pairwise subtractions, where the point on the left is constant and the
+sum of the weights is 0. -/
+lemma sum_smul_const_vsub_eq_neg_weighted_vsub (w : ι → k) (p₂ : ι → P) (p₁ : P)
+  (h : ∑ i in s, w i = 0) :
+  ∑ i in s, w i • (p₁ -ᵥ p₂ i) = -s.weighted_vsub p₂ w :=
+by rw [sum_smul_vsub_eq_weighted_vsub_sub, s.weighted_vsub_apply_const _ _ h, zero_sub]
+
 /-- A weighted sum of the results of subtracting a default base point
 from the given points, added to that base point, as an affine map on
 the weights.  This is intended to be used when the sum of the weights
@@ -226,6 +276,11 @@ lemma affine_combination_apply (w : ι → k) (p : ι → P) :
     s.weighted_vsub_of_point p (classical.choice S.nonempty) w +ᵥ (classical.choice S.nonempty) :=
 rfl
 
+/-- The value of `affine_combination`, where the given points are equal. -/
+@[simp] lemma affine_combination_apply_const (w : ι → k) (p : P) (h : ∑ i in s, w i = 1) :
+  s.affine_combination (λ _, p) w = p :=
+by rw [affine_combination_apply, s.weighted_vsub_of_point_apply_const, h, one_smul, vsub_vadd]
+
 /-- `affine_combination` gives the sum with any base point, when the
 sum of the weights is 1. -/
 lemma affine_combination_eq_weighted_vsub_of_point_vadd_of_sum_eq_one (w : ι → k) (p : ι → P)
@@ -305,6 +360,29 @@ lemma affine_combination_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) :
   (s₂.map e).affine_combination p w = s₂.affine_combination (p ∘ e) (w ∘ e) :=
 by simp_rw [affine_combination_apply, weighted_vsub_of_point_map]
 
+/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two `affine_combination`
+expressions. -/
+lemma sum_smul_vsub_eq_affine_combination_vsub (w : ι → k) (p₁ p₂ : ι → P) :
+  ∑ i in s, w i • (p₁ i -ᵥ p₂ i) = s.affine_combination p₁ w -ᵥ s.affine_combination p₂ w :=
+begin
+  simp_rw [affine_combination_apply, vadd_vsub_vadd_cancel_right],
+  exact s.sum_smul_vsub_eq_weighted_vsub_of_point_sub _ _ _ _
+end
+
+/-- A weighted sum of pairwise subtractions, where the point on the right is constant and the
+sum of the weights is 1. -/
+lemma sum_smul_vsub_const_eq_affine_combination_vsub (w : ι → k) (p₁ : ι → P) (p₂ : P)
+  (h : ∑ i in s, w i = 1) :
+  ∑ i in s, w i • (p₁ i -ᵥ p₂) = s.affine_combination p₁ w -ᵥ p₂ :=
+by rw [sum_smul_vsub_eq_affine_combination_vsub, affine_combination_apply_const _ _ _ h]
+
+/-- A weighted sum of pairwise subtractions, where the point on the left is constant and the
+sum of the weights is 1. -/
+lemma sum_smul_vsub_const_eq_vsub_affine_combination (w : ι → k) (p₂ : ι → P) (p₁ : P)
+  (h : ∑ i in s, w i = 1) :
+  ∑ i in s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ s.affine_combination p₂ w :=
+by rw [sum_smul_vsub_eq_affine_combination_vsub, affine_combination_apply_const _ _ _ h]
+
 variables {V}
 
 /-- Suppose an indexed family of points is given, along with a subset