# Spectrum of positive definite matrices #

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

### Positive semidefinite matrices #

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

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

source
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

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

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

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

source
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