posSemidef_iff_eigenvalues_nonneg

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

Похожие утверждения