trace_nonneg — Mathlib

English

Let A be a square complex matrix which is positive semidefinite. Then the trace of A is nonnegative: 0 ≤ tr(A).

Русский

Пусть A — квадратная матрица над комплексными числами, положительно полуопределенная. Тогда след(A) неотрицательно: tr(A) ≥ 0.

LaTeX

$$$\text{PosSemidef}(A) \implies 0 \le \operatorname{tr}(A)$$$

Lean4

theorem trace_nonneg {A : Matrix n n 𝕜} (hA : A.PosSemidef) : 0 ≤ A.trace := by
  classical
    simp [hA.isHermitian.trace_eq_sum_eigenvalues, ← map_sum, Finset.sum_nonneg (fun _ _ => hA.eigenvalues_nonneg _)]

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