Documentation

Mathlib.LinearAlgebra.AffineSpace.Matrix

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.

source
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
Instances For
    source
    @[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 : ι) :
    AffineBasis.toMatrix b q i j = (AffineBasis.coord b j) (q i)
    source
    @[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 ι] :
    AffineBasis.toMatrix b ⇑b = 1
    source
    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 : ι') :
    (Finset.sum Finset.univ fun (j : ι) => AffineBasis.toMatrix b q i j) = 1
    source
    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 : AffineBasis.toMatrix b 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.

    source
    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 * AffineBasis.toMatrix b 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.

    source
    @[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 ((AffineBasis.coords b₂) x) (AffineBasis.toMatrix b ⇑b₂) = (AffineBasis.coords b) x

    A change of basis formula for barycentric coordinates.

    See also AffineBasis.toMatrix_inv_vecMul_toMatrix.

    source
    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 ι] :
    AffineBasis.toMatrix b ⇑b₂ * AffineBasis.toMatrix b₂ ⇑b = 1
    source
    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 (AffineBasis.toMatrix b ⇑b₂)
    source
    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 (AffineBasis.toMatrix b p) ↔ AffineIndependent k p ∧ affineSpan k (Set.range p) = ⊤
    source
    @[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 ((AffineBasis.coords b) x) (AffineBasis.toMatrix b ⇑b₂)⁻¹ = (AffineBasis.coords b₂) x

    A change of basis formula for barycentric coordinates.

    See also AffineBasis.toMatrix_vecMul_coords.

    source
    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) :
    Matrix.det (AffineBasis.toMatrix b ⇑b₂) • (AffineBasis.coords b₂) x = (Matrix.cramer (Matrix.transpose (AffineBasis.toMatrix b ⇑b₂))) ((AffineBasis.coords b) 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.