Gram Matrices

This file defines Gram matrices and proves their positive semidefiniteness. Results require RCLike 𝕜.

Main definition

• Matrix.gram : the Matrix n n 𝕜 with ⟪v i, v j⟫ at i j : n, where v : n → E for an Inner 𝕜 E.

Main results

• Matrix.posSemidef_gram: Gram matrices are positive semidefinite.
• Matrix.posDef_gram_iff_linearIndependent: Linear independence of v is equivalent to positive definiteness of gram 𝕜 v.

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

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

@[simp]

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

@[simp]

theorem Matrix.gram_zero {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : gram 𝕜 0 = 0

@[simp]

theorem Matrix.gram_single {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq n] (i : n) (x : E) : gram 𝕜 (Pi.single i x) = single i i (inner 𝕜 x x)

theorem Matrix.submatrix_gram {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : n → E) {m : Set n} (f : ↑m → n) : (gram 𝕜 v).submatrix f f = gram 𝕜 (v ∘ f)

theorem Matrix.isHermitian_gram {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.star_dotProduct_gram_mulVec {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype n] (v : n → E) (x y : n → 𝕜) : star x ⬝ᵥ (gram 𝕜 v).mulVec y = inner 𝕜 (∑ i : n, x i • v i) (∑ i : n, y i • v i)

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

A Gram matrix is positive semidefinite.

theorem Matrix.linearIndependent_of_posDef_gram {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Finite n] {v : n → E} (h_gram : (gram 𝕜 v).PosDef) : LinearIndependent 𝕜 v

In a normed space, positive definiteness of gram 𝕜 v implies linear independence of v.

theorem Matrix.linearIndependent_of_det_gram_ne_zero {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype n] [DecidableEq n] {v : n → E} (h : (gram 𝕜 v).det ≠ 0) : LinearIndependent 𝕜 v

theorem Matrix.posDef_gram_of_linearIndependent {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Finite n] {v : n → E} (h_li : LinearIndependent 𝕜 v) : (gram 𝕜 v).PosDef

In a normed space, linear independence of v implies positive definiteness of gram 𝕜 v.

theorem Matrix.posDef_gram_iff_linearIndependent {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Finite n] {v : n → E} : (gram 𝕜 v).PosDef ↔ LinearIndependent 𝕜 v

In a normed space, linear independence of v is equivalent to positive definiteness of gram 𝕜 v.

theorem Matrix.det_gram_ne_zero_iff_linearIndependent {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype n] [DecidableEq n] {v : n → E} : (gram 𝕜 v).det ≠ 0 ↔ LinearIndependent 𝕜 v

theorem Matrix.gram_eq_conjTranspose_mul {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_5} [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : n → E) : gram 𝕜 v = (of fun (i : ι) (j : n) => (b.repr (v j)).ofLp i).conjTranspose * of fun (i : ι) (j : n) => (b.repr (v j)).ofLp i

@[simp]

theorem Matrix.gram_eq_one_iff_orthonormal {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq n] {v : n → E} : gram 𝕜 v = 1 ↔ Orthonormal 𝕜 v

theorem Matrix.posSemidef_opNorm_smul_gram_sub_gram {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (v : n → E) (f : E →L[𝕜] F) : (‖f‖ ^ 2 • gram 𝕜 v - gram 𝕜 (⇑f ∘ v)).PosSemidef

Inequality ‖f x‖ ≤ ‖f‖ * ‖x‖ lifted to Gram matrices.