eigenvalues_nonneg — Mathlib

English

For a PSD matrix, all eigenvalues are nonnegative.

Русский

Для ПСД-матрицы все собственные значения неотрицательны.

LaTeX

$$$A \text{ PosSemidef} \Rightarrow \forall i, \lambda_i(A) \ge 0$$$

Lean4

/-- The eigenvalues of a positive semi-definite matrix are non-negative -/
theorem eigenvalues_nonneg [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) (i : n) :
    0 ≤ hA.1.eigenvalues i :=
  (hA.re_dotProduct_nonneg _).trans_eq (hA.1.eigenvalues_eq _).symm

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