English
If d is a function from a finite index set to a ring R and we form the diagonal matrix diag(d), then diag(d) is positive semidefinite if and only if every diagonal entry d(i) is nonnegative.
Русский
Если d — функция с индексной области в кольцо R и образующая диагональная матрица diag(d), то diag(d) положительно полуопределена тогда и только тогда, когда все диагональные элементы d(i) неотрицательны.
LaTeX
$$$\mathrm{PosSemidef}(\mathrm{diagonal}(d)) \iff \forall i,\ 0 \le d(i)$$$
Lean4
/-- A matrix `M : Matrix n n R` is positive semidefinite if it is Hermitian and `xᴴ * M * x` is
nonnegative for all `x`. -/
def PosSemidef (M : Matrix n n R) :=
M.IsHermitian ∧ ∀ x : n → R, 0 ≤ star x ⬝ᵥ (M *ᵥ x)
