# 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₄} [] [] [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)
Instances For
@[simp]
theorem AffineBasis.toMatrix_apply {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [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₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] :
b.toMatrix b = 1
theorem AffineBasis.toMatrix_row_sum_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [] (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₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [] [Finite ι'] [] (p : ι'P) {A : Matrix ι ι' k} (hA : b.toMatrix p * A = 1) :

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₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [] [Fintype ι'] [] [] (p : ι'P) {A : Matrix ι ι' k} (hA : A * b.toMatrix p = 1) :

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₄} [] [] [Ring k] [Module k V] (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_inv_vecMul_toMatrix.

theorem AffineBasis.toMatrix_mul_toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] (b₂ : AffineBasis ι k P) [] :
b.toMatrix b₂ * b₂.toMatrix b = 1
theorem AffineBasis.isUnit_toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] (b₂ : AffineBasis ι k P) [] :
IsUnit (b.toMatrix b₂)
theorem AffineBasis.isUnit_toMatrix_iff {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] [] [] (p : ιP) :
IsUnit (b.toMatrix p) affineSpan k () =
@[simp]
theorem AffineBasis.toMatrix_inv_vecMul_toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [] [Module k V] [] [] (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₄} [] [] [] [Module k V] [] [] (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.