Spectrum of positive (semi)definite matrices

This file proves that eigenvalues of positive (semi)definite matrices are (nonnegative) positive.

Main definitions

• Matrix.toInnerProductSpace: the pre-inner product space on n → 𝕜 induced by a positive semi-definite matrix M, and is given by ⟪x, y⟫ = xᴴMy.

Positive semidefinite matrices

theorem Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : A.PosSemidef ↔ 0 ≤ hA.eigenvalues

A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative.

@[deprecated Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg (since := "2025-08-17")]

theorem Matrix.IsHermitian.posSemidef_of_eigenvalues_nonneg {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : 0 ≤ hA.eigenvalues → A.PosSemidef

Alias of the reverse direction of Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg.

---

A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative.

theorem Matrix.PosSemidef.eigenvalues_nonneg {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.PosSemidef) (i : n) : 0 ≤ ⋯.eigenvalues i

The eigenvalues of a positive semi-definite matrix are non-negative

theorem Matrix.PosSemidef.re_dotProduct_nonneg {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.PosSemidef) (x : n → 𝕜) : 0 ≤ RCLike.re (star x ⬝ᵥ A.mulVec x)

theorem Matrix.PosSemidef.det_nonneg {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.PosSemidef) : 0 ≤ A.det

theorem Matrix.PosSemidef.trace_eq_zero_iff {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.PosSemidef) : A.trace = 0 ↔ A = 0

theorem Matrix.eigenvalues_conjTranspose_mul_self_nonneg {m : Type u_1} {n : Type u_2} {𝕜 : Type u_3} [Fintype m] [Fintype n] [RCLike 𝕜] (A : Matrix m n 𝕜) [DecidableEq n] (i : n) : 0 ≤ ⋯.eigenvalues i

theorem Matrix.eigenvalues_self_mul_conjTranspose_nonneg {m : Type u_1} {n : Type u_2} {𝕜 : Type u_3} [Fintype m] [Fintype n] [RCLike 𝕜] (A : Matrix m n 𝕜) [DecidableEq m] (i : m) : 0 ≤ ⋯.eigenvalues i

Positive definite matrices

theorem Matrix.IsHermitian.posDef_iff_eigenvalues_pos {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) : A.PosDef ↔ ∀ (i : n), 0 < hA.eigenvalues i

A Hermitian matrix is positive-definite if and only if its eigenvalues are positive.

theorem Matrix.PosDef.re_dotProduct_pos {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.PosDef) {x : n → 𝕜} (hx : x ≠ 0) : 0 < RCLike.re (star x ⬝ᵥ A.mulVec x)

theorem Matrix.PosDef.eigenvalues_pos {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.PosDef) (i : n) : 0 < ⋯.eigenvalues i

The eigenvalues of a positive definite matrix are positive.

theorem Matrix.PosDef.det_pos {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.PosDef) : 0 < A.det

@[reducible, inline]

noncomputable abbrev Matrix.toSeminormedAddCommGroup {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] (M : Matrix n n 𝕜) (hM : M.PosSemidef) : SeminormedAddCommGroup (n → 𝕜)

A positive semi-definite matrix M induces a norm ‖x‖ = sqrt (re xᴴMx).

Equations

• M.toSeminormedAddCommGroup hM = InnerProductSpace.Core.toSeminormedAddCommGroup

@[reducible, inline]

noncomputable abbrev Matrix.toNormedAddCommGroup {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] (M : Matrix n n 𝕜) (hM : M.PosDef) : NormedAddCommGroup (n → 𝕜)

A positive definite matrix M induces a norm ‖x‖ = sqrt (re xᴴMx).

Equations

• M.toNormedAddCommGroup hM = InnerProductSpace.Core.toNormedAddCommGroup

def Matrix.toInnerProductSpace {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] (M : Matrix n n 𝕜) (hM : M.PosSemidef) : InnerProductSpace 𝕜 (n → 𝕜)

A positive semi-definite matrix M induces an inner product ⟪x, y⟫ = xᴴMy.

Equations

• M.toInnerProductSpace hM = InnerProductSpace.ofCore (Matrix.PosSemidef.preInnerProductSpace✝ hM)

@[deprecated Matrix.toNormedAddCommGroup (since := "2025-10-26")]

def Matrix.NormedAddCommGroup.ofMatrix {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] (M : Matrix n n 𝕜) (hM : M.PosDef) : NormedAddCommGroup (n → 𝕜)

Alias of Matrix.toNormedAddCommGroup.

---

A positive definite matrix M induces a norm ‖x‖ = sqrt (re xᴴMx).

Equations

• @Matrix.NormedAddCommGroup.ofMatrix = @Matrix.toNormedAddCommGroup

@[deprecated Matrix.toInnerProductSpace (since := "2025-10-26")]

def Matrix.InnerProductSpace.ofMatrix {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] (M : Matrix n n 𝕜) (hM : M.PosSemidef) : InnerProductSpace 𝕜 (n → 𝕜)

Alias of Matrix.toInnerProductSpace.

---

A positive semi-definite matrix M induces an inner product ⟪x, y⟫ = xᴴMy.

Equations

• @Matrix.InnerProductSpace.ofMatrix = @Matrix.toInnerProductSpace