Matrix results for barycentric co-ordinates

Results about the matrix of barycentric co-ordinates for a family of points in an affine space, with respect to some affine basis.

noncomputable def AffineBasis.toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} (q : ι' → P) : Matrix ι' ι k

Given an affine basis p, and a family of points q : ι' → P, this is the matrix whose rows are the barycentric coordinates of q with respect to p.

It is an affine equivalent of Basis.toMatrix.

Equations

• b.toMatrix q i j = (b.coord j) (q i)

@[simp]

theorem AffineBasis.toMatrix_apply {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} (q : ι' → P) (i : ι') (j : ι) : b.toMatrix q i j = (b.coord j) (q i)

@[simp]

theorem AffineBasis.toMatrix_self {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [DecidableEq ι] : b.toMatrix ⇑b = 1

theorem AffineBasis.toMatrix_row_sum_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [Fintype ι] (q : ι' → P) (i : ι') : ∑ j : ι, b.toMatrix q i j = 1

theorem AffineBasis.affineIndependent_of_toMatrix_right_inv {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [Fintype ι] [Finite ι'] [DecidableEq ι'] (p : ι' → P) {A : Matrix ι ι' k} (hA : b.toMatrix p * A = 1) : AffineIndependent k p

Given a family of points p : ι' → P and an affine basis b, if the matrix whose rows are the coordinates of p with respect b has a right inverse, then p is affine independent.

theorem AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [Finite ι] [Fintype ι'] [DecidableEq ι] [Nontrivial k] (p : ι' → P) {A : Matrix ι ι' k} (hA : A * b.toMatrix p = 1) : affineSpan k (Set.range p) = ⊤

Given a family of points p : ι' → P and an affine basis b, if the matrix whose rows are the coordinates of p with respect b has a left inverse, then p spans the entire space.

@[simp]

theorem AffineBasis.toMatrix_vecMul_coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Fintype ι] (b₂ : AffineBasis ι k P) (x : P) : Matrix.vecMul (b₂.coords x) (b.toMatrix ⇑b₂) = b.coords x

A change of basis formula for barycentric coordinates.

See also AffineBasis.toMatrix_inv_vecMul_toMatrix.

theorem AffineBasis.toMatrix_mul_toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Fintype ι] (b₂ : AffineBasis ι k P) [DecidableEq ι] : b.toMatrix ⇑b₂ * b₂.toMatrix ⇑b = 1

theorem AffineBasis.isUnit_toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Fintype ι] (b₂ : AffineBasis ι k P) [DecidableEq ι] : IsUnit (b.toMatrix ⇑b₂)

theorem AffineBasis.isUnit_toMatrix_iff {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [Ring k] [Module k V] (b : AffineBasis ι k P) [Fintype ι] [DecidableEq ι] [Nontrivial k] (p : ι → P) : IsUnit (b.toMatrix p) ↔ AffineIndependent k p ∧ affineSpan k (Set.range p) = ⊤

@[simp]

theorem AffineBasis.toMatrix_inv_vecMul_toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [CommRing k] [Module k V] [DecidableEq ι] [Fintype ι] (b : AffineBasis ι k P) (b₂ : AffineBasis ι k P) (x : P) : Matrix.vecMul (b.coords x) (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x

A change of basis formula for barycentric coordinates.

See also AffineBasis.toMatrix_vecMul_coords.

theorem AffineBasis.det_smul_coords_eq_cramer_coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [CommRing k] [Module k V] [DecidableEq ι] [Fintype ι] (b : AffineBasis ι k P) (b₂ : AffineBasis ι k P) (x : P) : (b.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂).transpose.cramer (b.coords x)

If we fix a background affine basis b, then for any other basis b₂, we can characterise the barycentric coordinates provided by b₂ in terms of determinants relative to b.