feat(linear_algebra/affine_space/barycentric_coords): define barycentric coordinates (#9472)

Author: ocfnash

src/linear_algebra/affine_space/barycentric_coords.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2021 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import linear_algebra.affine_space.independent
+
+/-!
+# Barycentric coordinates
+
+Suppose `P` is an affine space modelled on the module `V` over the ring `k`, and `p : ι → P` is an
+affine-independent family of points spanning `P`. Given this data, each point `q : P` may be written
+uniquely as an affine combination: `q = w₀ p₀ + w₁ p₁ + ⋯` for some (finitely-supported) weights
+`wᵢ`. For each `i : ι`, we thus have an affine map `P →ᵃ[k] k`, namely `q ↦ wᵢ`. This family of
+maps is known as the family of barycentric coordinates. It is defined in this file.
+
+## The construction
+
+Fixing `i : ι`, and allowing `j : ι` to range over the values `j ≠ i`, we obtain a basis `bᵢ` of `V`
+defined by `bᵢ j = p j -ᵥ p i`. Let `fᵢ j : V →ₗ[k] k` be the corresponding dual basis and let
+`fᵢ = ∑ j, fᵢ j : V →ₗ[k] k` be the corresponding "sum of all coordinates" form. Then the `i`th
+barycentric coordinate of `q : P` is `1 - fᵢ (q -ᵥ p i)`.
+
+## Main definitions
+
+ * `barycentric_coord`: the map `P →ᵃ[k] k` corresponding to `i : ι`.
+ * `barycentric_coord_apply_eq`: the behaviour of `barycentric_coord i` on `p i`.
+ * `barycentric_coord_apply_neq`: the behaviour of `barycentric_coord i` on `p j` when `j ≠ i`.
+ * `barycentric_coord_apply`: the behaviour of `barycentric_coord i` on `p j` for general `j`.
+ * `barycentric_coord_apply_combination`: the characterisation of `barycentric_coord i` in terms
+    of affine combinations, i.e., `barycentric_coord i (w₀ p₀ + w₁ p₁ + ⋯) = wᵢ`.
+
+## TODO
+
+ * Construct the affine equivalence between `P` and `{ f : ι →₀ k | f.sum = 1 }`.
+
+-/
+
+open_locale affine big_operators
+open set
+
+universes u₁ u₂ u₃ u₄
+
+variables {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄}
+variables [ring k] [add_comm_group V] [module k V] [affine_space V P]
+variables {p : ι → P} (h_ind : affine_independent k p) (h_tot : affine_span k (range p) = ⊤)
+include V h_ind h_tot
+
+/-- Given an affine-independent family of points spanning the point space `P`, if we single out one
+member of the family, we obtain a basis for the model space `V`.
+
+The basis correpsonding to the singled-out member `i : ι` is indexed by `{j : ι // j ≠ i}` and its
+`j`th element is `p j -ᵥ p i`. (See `basis_of_aff_ind_span_eq_top_apply`.) -/
+noncomputable def basis_of_aff_ind_span_eq_top (i : ι) : basis {j : ι // j ≠ i} k V :=
+basis.mk ((affine_independent_iff_linear_independent_vsub k p i).mp h_ind)
+begin
+  suffices : submodule.span k (range (λ (j : {x // x ≠ i}), p ↑j -ᵥ p i)) = vector_span k (range p),
+  { rw [this, ← direction_affine_span, h_tot, affine_subspace.direction_top], },
+  conv_rhs { rw ← image_univ, },
+  rw vector_span_image_eq_span_vsub_set_right_ne k p (mem_univ i),
+  congr,
+  ext v,
+  simp,
+end
+
+local notation `basis_of` := basis_of_aff_ind_span_eq_top h_ind h_tot
+
+@[simp] lemma basis_of_aff_ind_span_eq_top_apply (i : ι) (j : {j : ι // j ≠ i}) :
+  basis_of i j = p ↑j -ᵥ p i :=
+by simp [basis_of_aff_ind_span_eq_top]
+
+/-- The `i`th barycentric coordinate of a point. -/
+noncomputable def barycentric_coord (i : ι) : P →ᵃ[k] k :=
+{ to_fun    := λ q, 1 - (basis_of i).sum_coords (q -ᵥ p i),
+  linear    := -(basis_of i).sum_coords,
+  map_vadd' := λ q v, by rw [vadd_vsub_assoc, linear_map.map_add, vadd_eq_add, linear_map.neg_apply,
+    sub_add_eq_sub_sub_swap, add_comm, sub_eq_add_neg], }
+
+@[simp] lemma barycentric_coord_apply_eq (i : ι) :
+  barycentric_coord h_ind h_tot i (p i) = 1 :=
+by simp only [barycentric_coord, basis.coe_sum_coords, linear_equiv.map_zero, linear_equiv.coe_coe,
+  sub_zero, affine_map.coe_mk, finsupp.sum_zero_index, vsub_self]
+
+@[simp] lemma barycentric_coord_apply_neq (i j : ι) (h : j ≠ i) :
+  barycentric_coord h_ind h_tot i (p j) = 0 :=
+by rw [barycentric_coord, affine_map.coe_mk, ← subtype.coe_mk j h,
+  ← basis_of_aff_ind_span_eq_top_apply h_ind h_tot i ⟨j, h⟩, basis.sum_coords_self_apply, sub_self]
+
+lemma barycentric_coord_apply [decidable_eq ι] (i j : ι) :
+  barycentric_coord h_ind h_tot i (p j) = if i = j then 1 else 0 :=
+by { cases eq_or_ne i j; simp [h.symm], simp [h], }
+
+@[simp] lemma barycentric_coord_apply_combination
+  {s : finset ι} {i : ι} (hi : i ∈ s) {w : ι → k} (hw : s.sum w = 1) :
+  barycentric_coord h_ind h_tot i (s.affine_combination p w) = w i :=
+begin
+  classical,
+  simp only [barycentric_coord_apply, hi, finset.affine_combination_eq_linear_combination, if_true,
+    hw, mul_boole, function.comp_app, smul_eq_mul, s.sum_ite_eq, s.map_affine_combination p w hw],
+end

src/linear_algebra/affine_space/basic.lean

@@ -25,7 +25,8 @@ files:
 * `affine_equiv`: an equivalence between affine spaces that preserves the affine structure;
 * `affine_subspace`: a subset of an affine space closed w.r.t. affine combinations of points;
 * `affine_combination`: an affine combination of points;
-* `affine_independent`: affine independent set of points.
+* `affine_independent`: affine independent set of points;
+* `barycentric_coord`: the barycentric coordinate of a point.
 
 ## TODO
 
@@ -34,9 +35,6 @@ Some key definitions are not yet present.
 * Affine frames.  An affine frame might perhaps be represented as an `affine_equiv` to a `finsupp`
   (in the general case) or function type (in the finite-dimensional case) that gives the
   coordinates, with appropriate proofs of existence when `k` is a field.
-
-* Although results on affine combinations implicitly provide barycentric frames and coordinates,
-  there is no explicit representation of the map from a point to its coordinates.
  -/
 
 localized "notation `affine_space` := add_torsor" in affine

src/linear_algebra/basis.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
 -/
 import algebra.big_operators.finsupp
+import algebra.big_operators.finprod
 import data.fintype.card
 import linear_algebra.finsupp
 import linear_algebra.linear_independent
@@ -157,14 +158,42 @@ with respect to the basis `b`.
 finite-dimensional spaces it is the `ι`th basis vector of the dual space.
 -/
 @[simps]
-def coord (i : ι) : M →ₗ[R] R := (finsupp.lapply i) ∘ₗ ↑b.repr
+def coord : M →ₗ[R] R := (finsupp.lapply i) ∘ₗ ↑b.repr
 
 lemma forall_coord_eq_zero_iff {x : M} :
   (∀ i, b.coord i x = 0) ↔ x = 0 :=
 iff.trans
   (by simp only [b.coord_apply, finsupp.ext_iff, finsupp.zero_apply])
   b.repr.map_eq_zero_iff
 
+/-- The sum of the coordinates of an element `m : M` with respect to a basis. -/
+noncomputable def sum_coords : M →ₗ[R] R :=
+finsupp.lsum ℕ (λ i, linear_map.id) ∘ₗ (b.repr : M →ₗ[R] ι →₀ R)
+
+@[simp] lemma coe_sum_coords : (b.sum_coords : M → R) = λ m, (b.repr m).sum (λ i, id) :=
+rfl
+
+lemma coe_sum_coords_eq_finsum : (b.sum_coords : M → R) = λ m, ∑ᶠ i, b.coord i m :=
+begin
+  ext m,
+  simp only [basis.sum_coords, basis.coord, finsupp.lapply_apply, linear_map.id_coe,
+    linear_equiv.coe_coe, function.comp_app, finsupp.coe_lsum, linear_map.coe_comp,
+    finsum_eq_sum _ (b.repr m).finite_support, finsupp.sum, finset.finite_to_set_to_finset,
+    id.def, finsupp.fun_support_eq],
+end
+
+@[simp] lemma coe_sum_coords_of_fintype [fintype ι] : (b.sum_coords : M → R) = ∑ i, b.coord i :=
+begin
+  ext m,
+  simp only [sum_coords, finsupp.sum_fintype, linear_map.id_coe, linear_equiv.coe_coe, coord_apply,
+    id.def, fintype.sum_apply, implies_true_iff, eq_self_iff_true, finsupp.coe_lsum,
+    linear_map.coe_comp],
+end
+
+@[simp] lemma sum_coords_self_apply : b.sum_coords (b i) = 1 :=
+by simp only [basis.sum_coords, linear_map.id_coe, linear_equiv.coe_coe, id.def, basis.repr_self,
+  function.comp_app, finsupp.coe_lsum, linear_map.coe_comp, finsupp.sum_single_index]
+
 end coord
 
 section ext