# 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`.

source
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.

Equations

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

Instances For

source
@[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)
source
@[simp]
theorem Matrix.gram_zero {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
gram 𝕜 0 = 0
source
@[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)
source
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)
source
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.

source
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)
source
theorem Matrix.posSemidef_gram {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.

source
theorem Matrix.linearIndependent_of_posDef_gram {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype 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`.

source
theorem Matrix.posDef_gram_of_linearIndependent {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype 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`.

source
theorem Matrix.posDef_gram_iff_linearIndependent {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype 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`.