feat(linear_algebra/affine_space): affine combinations of points (#2979)

Some basic definitions and lemmas related to affine combinations of
points, in preparation for defining barycentric coordinates for use in
geometry.

This version for sums over a `fintype` is probably the most convenient
for geometrical uses (where the type will be `fin 3` in the case of a
triangle, or more generally `fin (n + 1)` for an n-simplex), but other
use cases may find that `finset` or `finsupp` versions of these
definitions are of use as well.

The definition `weighted_vsub` is expected to be used with weights
that sum to zero, and the definition `affine_combination` is expected
to be used with weights that sum to 1, but such a hypothesis is only
specified for lemmas that need it rather than for those definitions.
I expect that most nontrivial geometric uses of barycentric
coordinates will need to prove such a hypothesis at some point, but
that it will still be more convenient not to need to pass it to all
the definitions and trivial lemmas.




Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: jsm28

src/algebra/add_torsor.lean

@@ -5,6 +5,7 @@ Authors: Joseph Myers, Yury Kudryashov.
 -/
 import algebra.group.prod
 import algebra.group.type_tags
+import algebra.pi_instances
 import data.equiv.basic
 
 /-!
@@ -268,6 +269,32 @@ instance : add_torsor (G × G') (P × P') :=
 
 end prod
 
+namespace pi
+
+universes u v w
+variables {I : Type u} {fg : I → Type v} [∀ i, add_group (fg i)] {fp : I → Type w}
+
+open add_action add_torsor
+
+/-- A product of `add_torsor`s is an `add_torsor`. -/
+instance [T : ∀ i, add_torsor (fg i) (fp i)] : add_torsor (Π i, fg i) (Π i, fp i) :=
+{
+  vadd := λ g p, λ i, g i +ᵥ p i,
+  zero_vadd' := λ p, funext $ λ i, zero_vadd (fg i) (p i),
+  vadd_assoc' := λ g₁ g₂ p, funext $ λ i, vadd_assoc (fg i) (g₁ i) (g₂ i) (p i),
+  vsub := λ p₁ p₂, λ i, p₁ i -ᵥ p₂ i,
+  nonempty := ⟨λ i, classical.choice (T i).nonempty⟩,
+  vsub_vadd' := λ p₁ p₂, funext $ λ i, vsub_vadd (fg i) (p₁ i) (p₂ i),
+  vadd_vsub' := λ g p, funext $ λ i, vadd_vsub (fg i) (g i) (p i),
+}
+
+/-- Addition in a product of `add_torsor`s. -/
+@[simp] lemma vadd_apply [T : ∀ i, add_torsor (fg i) (fp i)] (x : Π i, fg i) (y : Π i, fp i)
+  {i : I} : (x +ᵥ y) i = x i +ᵥ y i
+:= rfl
+
+end pi
+
 namespace equiv
 
 variables (G : Type*) {P : Type*} [add_group G] [add_torsor G P]

src/linear_algebra/affine_space.lean

@@ -7,12 +7,14 @@ import algebra.add_torsor
 import linear_algebra.basis
 
 noncomputable theory
+open_locale big_operators
 
 /-!
 # Affine spaces
 
 This file defines affine spaces (over modules) and subspaces, affine
-maps, and the affine span of a set of points.
+maps, affine combinations of points, and the affine span of a set of
+points.
 
 ## Implementation notes
 
@@ -100,6 +102,158 @@ begin
   apply set.mem_of_mem_of_subset hp1p2 hp1p2s
 end
 
+section combination
+
+variables {k} {ι : Type*} [fintype ι]
+
+/-- A weighted sum of the results of subtracting a base point from the
+given points.  The main cases of interest are where the sum of the
+weights is 0, in which case the sum is independent of the choice of
+base point, and where the sum of the weights is 1, in which case the
+sum added to the base point is independent of the choice of base
+point. -/
+def weighted_vsub_of_point (w : ι → k) (p : ι → P) (b : P) : V := ∑ i, w i • (p i -ᵥ b)
+
+/-- `weighted_vsub_of_point` as a linear map on the weights. -/
+def weighted_vsub_of_point_linear (p : ι → P) (b : P) : (ι → k) →ₗ[k] V :=
+∑ i, (linear_map.proj i : (ι → k) →ₗ[k] k).smul_right (p i -ᵥ b)
+
+@[simp] lemma weighted_vsub_of_point_linear_apply (w : ι → k) (p : ι → P) (b : P) :
+  weighted_vsub_of_point_linear V p b w = weighted_vsub_of_point V w p b :=
+by simp [weighted_vsub_of_point_linear, linear_map.sum_apply, weighted_vsub_of_point]
+
+/-- The weighted sum when the weights are 0. -/
+@[simp] lemma weighted_vsub_of_point_zero (p : ι → P) (b : P) :
+  weighted_vsub_of_point V (0 : ι → k) p b = 0 :=
+by rw [← weighted_vsub_of_point_linear_apply, linear_map.map_zero]
+
+/-- The weighted sum, multiplied by a constant. -/
+lemma weighted_vsub_of_point_smul (r : k) (w : ι → k) (p : ι → P) (b : P) :
+  r • weighted_vsub_of_point V w p b = weighted_vsub_of_point V (r • w) p b :=
+by simp only [← weighted_vsub_of_point_linear_apply, linear_map.map_smul]
+
+/-- The weighted sum, negated. -/
+lemma weighted_vsub_of_point_neg (w : ι → k) (p : ι → P) (b : P) :
+  -weighted_vsub_of_point V w p b = weighted_vsub_of_point V (-w) p b :=
+by simp only [← weighted_vsub_of_point_linear_apply, linear_map.map_neg]
+
+/-- Adding two weighted sums. -/
+lemma weighted_vsub_of_point_add (w₁ w₂ : ι → k) (p : ι → P) (b : P) :
+  weighted_vsub_of_point V w₁ p b + weighted_vsub_of_point V w₂ p b =
+    weighted_vsub_of_point V (w₁ + w₂) p b :=
+by simp only [← weighted_vsub_of_point_linear_apply, linear_map.map_add]
+
+/-- Subtracting two weighted sums. -/
+lemma weighted_vsub_of_point_sub (w₁ w₂ : ι → k) (p : ι → P) (b : P) :
+  weighted_vsub_of_point V w₁ p b - weighted_vsub_of_point V w₂ p b =
+    weighted_vsub_of_point V (w₁ - w₂) p b :=
+by simp only [← weighted_vsub_of_point_linear_apply, linear_map.map_sub]
+
+/-- The weighted sum is independent of the base point when the sum of
+the weights is 0. -/
+lemma weighted_vsub_of_point_eq_of_sum_eq_zero (w : ι → k) (p : ι → P) (h : ∑ i, w i = 0)
+    (b₁ b₂ : P) : weighted_vsub_of_point V w p b₁ = weighted_vsub_of_point V w p b₂ :=
+begin
+  apply eq_of_sub_eq_zero,
+  erw ←finset.sum_sub_distrib,
+  conv_lhs {
+    congr,
+    skip,
+    funext,
+    rw [←smul_sub, vsub_sub_vsub_cancel_left]
+  },
+  rw [←finset.sum_smul, h, zero_smul]
+end
+
+/-- The weighted sum, added to the base point, is independent of the
+base point when the sum of the weights is 1. -/
+lemma weighted_vsub_of_point_vadd_eq_of_sum_eq_one (w : ι → k) (p : ι → P) (h : ∑ i, w i = 1)
+    (b₁ b₂ : P) : weighted_vsub_of_point V w p b₁ +ᵥ b₁ = weighted_vsub_of_point V w p b₂ +ᵥ b₂ :=
+begin
+  erw [←vsub_eq_zero_iff_eq V, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ←add_sub_assoc, add_comm,
+       add_sub_assoc, ←finset.sum_sub_distrib],
+  conv_lhs {
+    congr,
+    skip,
+    congr,
+    skip,
+    funext,
+    rw [←smul_sub, vsub_sub_vsub_cancel_left]
+  },
+  rw [←finset.sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]
+end
+
+/-- A weighted sum of the results of subtracting a default base point
+from the given points.  This is intended to be used when the sum of
+the weights is 0; that condition is specified as a hypothesis on those
+lemmas that require it. -/
+def weighted_vsub (w : ι → k) (p : ι → P) : V :=
+weighted_vsub_of_point V w p (classical.choice S.nonempty)
+
+/-- `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)
+    (h : ∑ i, w i = 0) (b : P) : weighted_vsub V w p = weighted_vsub_of_point V w p b :=
+weighted_vsub_of_point_eq_of_sum_eq_zero V w p h _ _
+
+/-- The weighted sum when the weights are 0. -/
+@[simp] lemma weighted_vsub_zero (p : ι → P) : weighted_vsub V (0 : ι → k) p = 0 :=
+weighted_vsub_of_point_zero V p _
+
+/-- The weighted sum, multiplied by a constant. -/
+lemma weighted_vsub_smul (r : k) (w : ι → k) (p : ι → P) :
+  r • weighted_vsub V w p = weighted_vsub V (r • w) p :=
+weighted_vsub_of_point_smul V r w p _
+
+/-- The weighted sum, negated. -/
+lemma weighted_vsub_neg (w : ι → k) (p : ι → P) :
+  -weighted_vsub V w p = weighted_vsub V (-w) p :=
+weighted_vsub_of_point_neg V w p _
+
+/-- Adding two weighted sums. -/
+lemma weighted_vsub_add (w₁ w₂ : ι → k) (p : ι → P) :
+  weighted_vsub V w₁ p + weighted_vsub V w₂ p = weighted_vsub V (w₁ + w₂) p :=
+weighted_vsub_of_point_add V w₁ w₂ p _
+
+/-- Subtracting two weighted sums. -/
+lemma weighted_vsub_sub (w₁ w₂ : ι → k) (p : ι → P) :
+  weighted_vsub V w₁ p - weighted_vsub V w₂ p = weighted_vsub V (w₁ - w₂) p :=
+weighted_vsub_of_point_sub V w₁ w₂ p _
+
+/-- A weighted sum of the results of subtracting a default base point
+from the given points, added to that base point.  This is intended to
+be used when the sum of the weights is 1, in which case it is an
+affine combination (barycenter) of the points with the given weights;
+that condition is specified as a hypothesis on those lemmas that
+require it. -/
+def affine_combination (w : ι → k) (p : ι → P) : P :=
+weighted_vsub_of_point V w p (classical.choice S.nonempty) +ᵥ (classical.choice S.nonempty)
+
+/-- `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)
+    (h : ∑ i, w i = 1) (b : P) : affine_combination V w p = weighted_vsub_of_point V w p b +ᵥ b :=
+weighted_vsub_of_point_vadd_eq_of_sum_eq_one V w p h _ _
+
+/-- Adding a `weighted_vsub` to an `affine_combination`. -/
+lemma weighted_vsub_vadd_affine_combination (w₁ w₂ : ι → k) (p : ι → P) :
+  weighted_vsub V w₁ p +ᵥ affine_combination V w₂ p = affine_combination V (w₁ + w₂) p :=
+begin
+  erw vadd_assoc,
+  congr,
+  exact weighted_vsub_add V w₁ w₂ p
+end
+
+/-- Subtracting two `affine_combination`s. -/
+lemma affine_combination_vsub (w₁ w₂ : ι → k) (p : ι → P) :
+  affine_combination V w₁ p -ᵥ affine_combination V w₂ p = weighted_vsub V (w₁ - w₂) p :=
+begin
+  erw vadd_vsub_vadd_cancel_right,
+  exact weighted_vsub_sub V w₁ w₂ p
+end
+
+end combination
+
 end affine_space
 
 open add_torsor affine_space
@@ -464,6 +618,23 @@ rfl
 
 end affine_map
 
+namespace affine_map
+variables {k : Type*} (V : Type*) (P : Type*) [comm_ring k] [add_comm_group V] [module k V]
+variables [affine_space k V P] {ι : Type*} [fintype ι]
+
+-- TODO: define `affine_map.proj`, `affine_map.fst`, `affine_map.snd`
+/-- A weighted sum, as an affine map on the points involved. -/
+def weighted_vsub_of_point (w : ι → k) : affine_map k ((ι → V) × V) ((ι → P) × P) V V :=
+{ to_fun := λ p, weighted_vsub_of_point _ w p.fst p.snd,
+  linear := ∑ i, w i • ((linear_map.proj i).comp (linear_map.fst _ _ _) - linear_map.snd _ _ _),
+  map_vadd' := begin
+    rintros ⟨p, b⟩ ⟨v, b'⟩,
+    simp [linear_map.sum_apply, weighted_vsub_of_point, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc,
+      add_sub, ← sub_add_eq_add_sub, smul_add, finset.sum_add_distrib]
+  end }
+
+end affine_map
+
 namespace linear_map
 
 variables {k : Type*} {V₁ : Type*} {V₂ : Type*} [ring k] [add_comm_group V₁] [module k V₁]