feat(LinearAlgebra/Matrix/PosDef): trace of Hermitian matrix is sum of its eigenvalues (#28730)

Trace of Hermitian matrix is sum of its eigenvalues and trace is non-negative for positive semi-definite and positive for positive definite.

Author: themathqueen

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -171,6 +171,11 @@ lemma 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
 
+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 _)]
+
 theorem det_nonneg [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosSemidef) :
     0 ≤ M.det := by
   rw [hM.isHermitian.det_eq_prod_eigenvalues]
@@ -528,6 +533,11 @@ lemma _root_.Matrix.IsHermitian.posDef_iff_eigenvalues_pos [DecidableEq n] {A :
   rw [vecMul_injective_iff_isUnit, ← unitary.val_toUnits_apply]
   exact Units.isUnit _
 
+theorem trace_pos [Nonempty n] {A : Matrix n n 𝕜} (hA : A.PosDef) : 0 < A.trace := by
+  classical
+  simp [hA.isHermitian.trace_eq_sum_eigenvalues, ← map_sum,
+    Finset.sum_pos (fun _ _ => hA.eigenvalues_pos _)]
+
 theorem det_pos [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : 0 < det M := by
   rw [hM.isHermitian.det_eq_prod_eigenvalues]
   apply Finset.prod_pos

Mathlib/LinearAlgebra/Matrix/Spectrum.lean

@@ -170,6 +170,11 @@ lemma exists_eigenvector_of_ne_zero (hA : IsHermitian A) (h_ne : A ≠ 0) :
   obtain ⟨i, hi⟩ := Function.ne_iff.mp this
   exact ⟨_, _, hi, hA.eigenvectorBasis.orthonormal.ne_zero i, hA.mulVec_eigenvectorBasis i⟩
 
+theorem trace_eq_sum_eigenvalues [DecidableEq n] (hA : A.IsHermitian) :
+    A.trace = ∑ i, (hA.eigenvalues i : 𝕜) := by
+  conv_lhs => rw [hA.spectral_theorem, trace_mul_cycle]
+  simp
+
 end IsHermitian
 
 end Matrix