feat(analysis/normed_space/real_inner_product,geometry/euclidean): in…

…ner products of weighted subtractions (#3203)

Express the inner product of two weighted sums, where the weights in
each sum add to 0, in terms of the norms of pairwise differences.
Thus, express inner products for vectors expressed in terms of
`weighted_vsub` and distances for points expressed in terms of
`affine_combination`.

This is a general form of the standard formula for a distance between
points expressed in terms of barycentric coordinates: if the
difference between the normalized barycentric coordinates (with
respect to triangle ABC) for two points is (x, y, z) then the squared
distance between them is -(a^2 yz + b^2 zx + c^2 xy).

Although some of the lemmas are given with the two vectors expressed
as sums over different indexed families of vectors or points (since
nothing in the statement or proof depends on them being the same), I
expect almost all uses will be in cases where the two indexed families
are the same and only the weights vary.

src/analysis/normed_space/real_inner_product.lean

@@ -600,6 +600,20 @@ begin
     exact inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul hx hr }
 end
 
+/-- The inner product of two weighted sums, where the weights in each
+sum add to 0, in terms of the norms of pairwise differences. -/
+lemma inner_sum_smul_sum_smul_of_sum_eq_zero {ι₁ : Type*} {s₁ : finset ι₁} {w₁ : ι₁ → ℝ}
+    (v₁ : ι₁ → α) (h₁ : ∑ i in s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : finset ι₂} {w₂ : ι₂ → ℝ}
+    (v₂ : ι₂ → α) (h₂ : ∑ i in s₂, w₂ i = 0) :
+  inner (∑ i₁ in s₁, w₁ i₁ • v₁ i₁) (∑ i₂ in s₂, w₂ i₂ • v₂ i₂) =
+    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (∥v₁ i₁ - v₂ i₂∥ * ∥v₁ i₁ - v₂ i₂∥)) / 2 :=
+by simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right,
+            inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two,
+            ←div_sub_div_same, ←div_add_div_same, mul_sub_left_distrib, left_distrib,
+            finset.sum_sub_distrib, finset.sum_add_distrib, ←finset.mul_sum, ←finset.sum_mul,
+            h₁, h₂, zero_mul, mul_zero, finset.sum_const_zero, zero_add, zero_sub, finset.mul_sum,
+            neg_div, finset.sum_div, mul_div_assoc, mul_assoc]
+
 end norm
 
 /-! ### Inner product space structure on product spaces -/

src/geometry/euclidean.lean

@@ -5,9 +5,11 @@ Author: Joseph Myers.
 -/
 import analysis.normed_space.real_inner_product
 import analysis.normed_space.add_torsor
+import linear_algebra.affine_space
 import tactic.interval_cases
 
 noncomputable theory
+open_locale big_operators
 open_locale classical
 open_locale real
 
@@ -645,4 +647,40 @@ begin
                                                 (λ he, h2 ((vsub_eq_zero_iff_eq V).1 he))
 end
 
+/-- The inner product of two vectors given with `weighted_vsub`, in
+terms of the pairwise distances. -/
+lemma inner_weighted_vsub {ι₁ : Type*} {s₁ : finset ι₁} {w₁ : ι₁ → ℝ} (p₁ : ι₁ → P)
+    (h₁ : ∑ i in s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P)
+    (h₂ : ∑ i in s₂, w₂ i = 0) :
+  inner (s₁.weighted_vsub V p₁ w₁) (s₂.weighted_vsub V p₂ w₂) =
+    (-∑ i₁ in s₁, ∑ i₂ in s₂,
+      w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2 :=
+begin
+  rw [finset.weighted_vsub_apply, finset.weighted_vsub_apply,
+      inner_sum_smul_sum_smul_of_sum_eq_zero _ h₁ _ h₂],
+  simp_rw [vsub_sub_vsub_cancel_right],
+  congr,
+  ext i₁,
+  congr,
+  ext i₂,
+  rw dist_eq_norm V (p₁ i₁) (p₂ i₂)
+end
+
+/-- The distance between two points given with `affine_combination`,
+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) :
+  dist (s.affine_combination V w₁ p) (s.affine_combination V w₂ p) *
+    dist (s.affine_combination V w₁ p) (s.affine_combination V w₂ p) =
+    (-∑ 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 V (s.affine_combination V w₁ p) (s.affine_combination V w₂ p),
+      ←inner_self_eq_norm_square, 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] },
+  exact inner_weighted_vsub V p h p h
+end
+
 end euclidean_geometry

src/linear_algebra/affine_space.lean

@@ -192,6 +192,16 @@ is specified as a hypothesis on those lemmas that require it. -/
 def weighted_vsub (p : ι → P) : (ι → k) →ₗ[k] V :=
 s.weighted_vsub_of_point V p (classical.choice S.nonempty)
 
+/-- Applying `weighted_vsub` with given weights.  This is for the case
+where a result involving a default base point is OK (for example, when
+that base point will cancel out later); a more typical use case for
+`weighted_vsub` would involve selecting a preferred base point with
+`weighted_vsub_eq_weighted_vsub_of_point_of_sum_eq_zero` and then
+using `weighted_vsub_of_point_apply`. -/
+lemma weighted_vsub_apply (w : ι → k) (p : ι → P) :
+  s.weighted_vsub V p w = ∑ i in s, w i • (p i -ᵥ (classical.choice S.nonempty)) :=
+by simp [weighted_vsub, linear_map.sum_apply]
+
 /-- `weighted_vsub` gives the sum of the results of subtracting any
 base point, when the sum of the weights is 0. -/
 lemma weighted_vsub_eq_weighted_vsub_of_point_of_sum_eq_zero (w : ι → k) (p : ι → P)