Gram Matrices

This file defines Gram matrices and proves their positive semi-definiteness. Results require RCLike 𝕜.

Main definition

• Matrix.Gram : the Matrix n n 𝕜 with ⟪v i, v j⟫ at i j : n, where v : n → α for an InnerProductSpace 𝕜 α.

Main results

• Matrix.IsGram.PosSemidef Gram matrices are positive semi-definite.

def Matrix.gram {E : Type u_1} {n : Type u_2} (𝕜 : Type u_5) [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : n → E) : Matrix n n 𝕜

The entries of a Gram matrix are inner products of vectors in an inner product space.

Equations

• Matrix.gram 𝕜 v = Matrix.of fun (i j : n) => inner 𝕜 (v i) (v j)

theorem Matrix.gram_apply {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : n → E} (i j : n) : gram 𝕜 v i j = inner 𝕜 (v i) (v j)

For the matrix gram 𝕜 v, the entry at i j : n equals ⟪v i, v j⟫.

theorem Matrix.gram_isHermitian {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : n → E} : (gram 𝕜 v).IsHermitian

A Gram matrix is Hermitian.

theorem Matrix.gram_posSemidef {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype n] {v : n → E} : (gram 𝕜 v).PosSemidef

A Gram matrix is positive semidefinite.