English
If A is positive semidefinite (A ∈ M_n(𝕜)), then every eigenvalue of A is a nonnegative real number; equivalently, the spectrum of A lies in the nonnegative real axis.
Русский
Если A положительно полуопределена, то все ее собственные значения неотрицательны и вещественны; спектр A лежит в множестве неотрицательных вещественных чисел.
LaTeX
$$$\mathrm{spec}(A) \subseteq \{\lambda \in \mathbb{R} \mid \lambda \ge 0\}. $$$
Lean4
theorem instNonnegSpectrumClass : NonnegSpectrumClass ℝ (Matrix n n 𝕜) where
quasispectrum_nonneg_of_nonneg A
hA := by
classical
simp only [quasispectrum_eq_spectrum_union_zero ℝ A, Set.union_singleton, Set.mem_insert_iff, forall_eq_or_imp,
le_refl, true_and]
intro x hx
obtain ⟨i, rfl⟩ := Set.ext_iff.mp hA.posSemidef.1.spectrum_real_eq_range_eigenvalues x |>.mp hx
exact hA.posSemidef.eigenvalues_nonneg _
