Gram matrices and standard-basis dot products.

@[simp]

theorem Vector.dotProduct_unit_unit {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (i j : Fin n) : (unit R i).dotProduct (unit R j) = if i = j then 1 else 0

Dot product of standard basis vectors.

def Hex.Matrix.gramMatrix {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) : Matrix R n n

Gram matrix of the rows of a dense matrix.

Equations

• M.gramMatrix = Hex.Matrix.ofFn fun (i j : Fin n) => (M.row i).dotProduct (M.row j)

theorem Hex.Matrix.getElem_gramMatrix {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) (i j : Fin n) : M.gramMatrix[i][j] = (M.row i).dotProduct (M.row j)

Entry characterization for the Gram matrix of the rows of a dense matrix.

@[simp]

theorem Hex.Matrix.row_gramMatrix {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) (i : Fin n) : M.gramMatrix.row i = Vector.ofFn fun (j : Fin n) => (M.row i).dotProduct (M.row j)

Row i of the Gram matrix pairs row M i against every row of M.

@[simp]

theorem Hex.Matrix.col_gramMatrix {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] (M : Matrix R n m) (j : Fin n) : M.gramMatrix.col j = Vector.ofFn fun (i : Fin n) => (M.row i).dotProduct (M.row j)

Column j of the Gram matrix pairs every row of M against row M j. The Gram matrix is symmetric, so this matches row_gramMatrix.

@[simp]

theorem Hex.Matrix.gramMatrix_identity {R : Type u} [Lean.Grind.CommRing R] {n : Nat} : (Matrix.identity n).gramMatrix = Matrix.identity n

The Gram matrix of the identity is the identity.