English
For a matrix A, A is positive semidefinite if and only if A is Hermitian and its spectrum is contained in the nonnegative reals.
Русский
Для матрицы A условие A положительно полуопределена эквивалентно тому, что A эрмитова и ее спектр лежит в неотрицательных вещественных числах.
LaTeX
$$$A^{PosSemidef} \iff (A^{IsHermitian} \land spectrum \subseteq \{a:\mathbb{R} \mid 0 \le a\}).$$$
Lean4
theorem posSemidef_iff_isHermitian_and_spectrum_nonneg [DecidableEq n] {A : Matrix n n 𝕜} :
A.PosSemidef ↔ A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a : 𝕜 | 0 ≤ a} :=
by
refine ⟨fun h => ⟨h.isHermitian, fun a => ?_⟩, fun ⟨h1, h2⟩ => ?_⟩
· simp only [h.isHermitian.spectrum_eq_image_range, Set.mem_image, Set.mem_range, exists_exists_eq_and,
Set.mem_setOf_eq, forall_exists_index]
rintro i rfl
exact_mod_cast h.eigenvalues_nonneg _
· rw [h1.posSemidef_iff_eigenvalues_nonneg]
intro i
simpa [h1.spectrum_eq_image_range] using @h2 (h1.eigenvalues i)
