Spectrum of positive definite matrices

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

Positive semidefinite matrices

theorem Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n 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 𝕜] [DecidableEq n] {A : Matrix n 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 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) (i : n) : 0 ≤ ⋯.eigenvalues i

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

theorem Matrix.PosSemidef.det_nonneg {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosSemidef) : 0 ≤ M.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 𝕜] [DecidableEq n] {A : Matrix n 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.eigenvalues_pos {n : Type u_2} {𝕜 : Type u_3} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n 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 𝕜] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : 0 < M.det