English
A Hermitian matrix is positive semidefinite iff all its eigenvalues are nonnegative.
Русский
Гермитова матрица положительно полуопределена тогда и только тогда, когда все её собственные значения неотрицательны.
LaTeX
$$PosSemidef(A) ↔ 0 ≤ eigenvalues(A) (for Hermitian A)$$
Lean4
/-- A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative. -/
theorem posSemidef_iff_eigenvalues_nonneg [DecidableEq n] {A : Matrix n n 𝕜} (hA : IsHermitian A) :
PosSemidef A ↔ 0 ≤ hA.eigenvalues :=
by
refine ⟨fun h => h.eigenvalues_nonneg, fun h => ?_⟩
rw [hA.spectral_theorem]
refine (posSemidef_diagonal_iff.mpr ?_).mul_mul_conjTranspose_same _
simpa using h