English
A Hermitian matrix is positive definite if and only if all its eigenvalues are positive.
Русский
Гермианова матрица положительно определена тогда и только тогда, когда все её собственные значения положительны.
LaTeX
$$$$ A^{\\mathrm{IsHermitian}} \\Rightarrow \\operatorname{PosDef}(A) \\iff \\forall i, 0 < A_{\\text{eigenvalues}}(i). $$$$
Lean4
/-- A Hermitian matrix is positive-definite if and only if its eigenvalues are positive. -/
theorem _root_.Matrix.IsHermitian.posDef_iff_eigenvalues_pos [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :
A.PosDef ↔ ∀ i, 0 < hA.eigenvalues i :=
by
refine ⟨fun h => h.eigenvalues_pos, fun h => ?_⟩
rw [hA.spectral_theorem]
refine (posDef_diagonal_iff.mpr <| by simpa using h).mul_mul_conjTranspose_same ?_
rw [vecMul_injective_iff_isUnit, ← unitary.val_toUnits_apply]
exact Units.isUnit _
