feat: Positivity/Nonnegativity of Eigenvalues of PosDef/PosSemidef Matrices (#6368)

Two lemmas:

- `Matrix.PosDef.eigenvalues_pos`: $$A \in k^{n\times n}, A > 0 \implies \lambda (A) >0$$
- `Matrix.PosSemidef.eigenvalues_nonneg`: $$A \in k^{n\times n}, A \geq 0 \implies \lambda (A) \geq 0$$


Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: MohanadAhmed

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -104,6 +104,17 @@ theorem posSemidef_conjTranspose_mul_self (A : Matrix m n 𝕜) : Matrix.PosSemi
 theorem posSemidef_self_mul_conjTranspose (A : Matrix m n 𝕜) : Matrix.PosSemidef (A ⬝ Aᴴ) :=
   by simpa only [conjTranspose_conjTranspose] using posSemidef_conjTranspose_mul_self Aᴴ
 
+/-- The eigenvalues of a positive definite matrix are positive -/
+lemma PosDef.eigenvalues_pos [DecidableEq n] [DecidableEq 𝕜] {A : Matrix n n 𝕜}
+    (hA : Matrix.PosDef A) (i : n) : 0 < hA.1.eigenvalues i := by
+  rw [hA.1.eigenvalues_eq, hA.1.transpose_eigenvectorMatrix_apply]
+  exact hA.2 _ <| hA.1.eigenvectorBasis.orthonormal.ne_zero i
+
+/-- The eigenvalues of a positive semi-definite matrix are non-negative -/
+lemma PosSemidef.eigenvalues_nonneg [DecidableEq n] [DecidableEq 𝕜] {A : Matrix n n 𝕜}
+    (hA : Matrix.PosSemidef A) (i : n) : 0 ≤ hA.1.eigenvalues i :=
+  (hA.2 _).trans_eq (hA.1.eigenvalues_eq _).symm
+
 namespace PosDef
 
 variable {M : Matrix n n ℝ} (hM : M.PosDef)

Mathlib/LinearAlgebra/Matrix/Spectrum.lean

@@ -76,6 +76,11 @@ theorem eigenvectorMatrix_apply (i j : n) : hA.eigenvectorMatrix i j = hA.eigenv
     PiLp.basisFun_repr]
 #align matrix.is_hermitian.eigenvector_matrix_apply Matrix.IsHermitian.eigenvectorMatrix_apply
 
+/-- The columns of `Matrix.IsHermitian.eigenVectorMatrix` form the basis-/
+theorem transpose_eigenvectorMatrix_apply (i : n) :
+    hA.eigenvectorMatrixᵀ i = hA.eigenvectorBasis i :=
+  funext <| fun j => eigenvectorMatrix_apply hA j i
+
 theorem eigenvectorMatrixInv_apply (i j : n) :
     hA.eigenvectorMatrixInv i j = star (hA.eigenvectorBasis i j) := by
   rw [eigenvectorMatrixInv, Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply,