chore(LinearAlgebra/Matrix): import less analysis (#31480)

Move the definition of eigenvalues of hermitian matrices to `Analysis.Matrix`, and the corresponding lemmas about positive (semi)definite matrices too. Some lemmas could be generalised instead of moved, and I have done so.

Ultimately, it would be great for `LinearAlgebra.Matrix` to import no analysis at all. But this is a longer term goal.

Author: YaelDillies

Mathlib.lean

@@ -1805,6 +1805,8 @@ import Mathlib.Analysis.LocallyConvex.WithSeminorms
 import Mathlib.Analysis.Matrix
 import Mathlib.Analysis.Matrix.Normed
 import Mathlib.Analysis.Matrix.Order
+import Mathlib.Analysis.Matrix.PosDef
+import Mathlib.Analysis.Matrix.Spectrum
 import Mathlib.Analysis.MeanInequalities
 import Mathlib.Analysis.MeanInequalitiesPow
 import Mathlib.Analysis.MellinInversion
@@ -4457,7 +4459,6 @@ import Mathlib.LinearAlgebra.Matrix.SchurComplement
 import Mathlib.LinearAlgebra.Matrix.SemiringInverse
 import Mathlib.LinearAlgebra.Matrix.SesquilinearForm
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
-import Mathlib.LinearAlgebra.Matrix.Spectrum
 import Mathlib.LinearAlgebra.Matrix.StdBasis
 import Mathlib.LinearAlgebra.Matrix.Swap
 import Mathlib.LinearAlgebra.Matrix.Symmetric

Mathlib/Algebra/Star/Basic.lean

@@ -172,6 +172,11 @@ variable (R) in
 theorem star_one [MulOneClass R] [StarMul R] : star (1 : R) = 1 :=
   op_injective <| (starMulEquiv : R ≃* Rᵐᵒᵖ).map_one.trans op_one.symm
 
+@[simp]
+lemma Pi.star_mulSingle {ι : Type*} {R : ι → Type*} [DecidableEq ι] [∀ i, MulOneClass (R i)]
+    [∀ i, StarMul (R i)] (i : ι) (r : R i) : star (mulSingle i r) = mulSingle i (star r) := by
+  ext; exact apply_mulSingle (fun _ ↦ star) (fun _ ↦ star_one _) ..
+
 @[simp]
 theorem star_pow [Monoid R] [StarMul R] (x : R) (n : ℕ) : star (x ^ n) = star x ^ n :=
   op_injective <|
@@ -232,6 +237,11 @@ variable (R) in
 theorem star_zero [AddMonoid R] [StarAddMonoid R] : star (0 : R) = 0 :=
   (starAddEquiv : R ≃+ R).map_zero
 
+@[simp]
+lemma Pi.star_single {ι : Type*} {R : ι → Type*} [DecidableEq ι] [∀ i, AddMonoid (R i)]
+    [∀ i, StarAddMonoid (R i)] (i : ι) (r : R i) : star (single i r) = single i (star r) := by
+  ext; exact apply_single (fun _ ↦ star) (fun _ ↦ star_zero _) ..
+
 @[simp]
 theorem star_eq_zero [AddMonoid R] [StarAddMonoid R] {x : R} : star x = 0 ↔ x = 0 :=
   starAddEquiv.map_eq_zero_iff (M := R)

Mathlib/Analysis/InnerProductSpace/Positive.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
-import Mathlib.Analysis.InnerProductSpace.Adjoint
 import Mathlib.Analysis.InnerProductSpace.Spectrum
 import Mathlib.LinearAlgebra.Matrix.PosDef
 

Mathlib/Analysis/Matrix/Order.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Monica Omar
 -/
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
+import Mathlib.Analysis.Matrix.PosDef
 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
 import Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus
-import Mathlib.LinearAlgebra.Matrix.PosDef
 
 /-!
 # The partial order on matrices

Mathlib/Analysis/Matrix/PosDef.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2022 Alexander Bentkamp. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Bentkamp, Mohanad Ahmed
+-/
+import Mathlib.Analysis.Matrix.Spectrum
+import Mathlib.LinearAlgebra.Matrix.PosDef
+
+/-!
+# Spectrum of positive definite matrices
+
+This file proves that eigenvalues of positive (semi)definite matrices are (nonnegative) positive.
+-/
+
+open WithLp
+open scoped ComplexOrder
+
+namespace Matrix
+variable {m n 𝕜 : Type*} [Fintype m] [Fintype n] [RCLike 𝕜]
+
+/-! ### Positive semidefinite matrices -/
+
+namespace PosSemidef
+
+/-- The eigenvalues of a positive semi-definite matrix are non-negative -/
+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
+
+lemma det_nonneg [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosSemidef) :
+    0 ≤ M.det := by
+  rw [hM.isHermitian.det_eq_prod_eigenvalues]
+  exact Finset.prod_nonneg fun i _ ↦ by simpa using hM.eigenvalues_nonneg i
+
+end PosSemidef
+
+lemma eigenvalues_conjTranspose_mul_self_nonneg (A : Matrix m n 𝕜) [DecidableEq n] (i : n) :
+    0 ≤ (isHermitian_conjTranspose_mul_self A).eigenvalues i :=
+  (posSemidef_conjTranspose_mul_self _).eigenvalues_nonneg _
+
+lemma eigenvalues_self_mul_conjTranspose_nonneg (A : Matrix m n 𝕜) [DecidableEq m] (i : m) :
+    0 ≤ (isHermitian_mul_conjTranspose_self A).eigenvalues i :=
+  (posSemidef_self_mul_conjTranspose _).eigenvalues_nonneg _
+
+/-- A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative. -/
+lemma IsHermitian.posSemidef_iff_eigenvalues_nonneg [DecidableEq n] {A : Matrix n n 𝕜}
+    (hA : IsHermitian A) : PosSemidef A ↔ 0 ≤ hA.eigenvalues := by
+  refine ⟨fun h => h.eigenvalues_nonneg, fun h => ?_⟩
+  rw [hA.spectral_theorem]
+  refine (posSemidef_diagonal_iff.mpr ?_).mul_mul_conjTranspose_same _
+  simpa using h
+
+@[deprecated (since := "2025-08-17")] alias ⟨_, IsHermitian.posSemidef_of_eigenvalues_nonneg⟩ :=
+  IsHermitian.posSemidef_iff_eigenvalues_nonneg
+
+lemma PosSemidef.trace_eq_zero_iff {A : Matrix n n 𝕜} (hA : A.PosSemidef) :
+    A.trace = 0 ↔ A = 0 := by
+  refine ⟨fun h => ?_, fun h => h ▸ trace_zero n 𝕜⟩
+  classical
+  simp_rw [hA.isHermitian.trace_eq_sum_eigenvalues, ← RCLike.ofReal_sum,
+    RCLike.ofReal_eq_zero, Finset.sum_eq_zero_iff_of_nonneg (s := Finset.univ)
+      (by simpa using hA.eigenvalues_nonneg), Finset.mem_univ, true_imp_iff] at h
+  exact funext_iff.eq ▸ hA.isHermitian.eigenvalues_eq_zero_iff.mp <| h
+
+/-! ### Positive definite matrices -/
+
+namespace PosDef
+
+/-- The eigenvalues of a positive definite matrix are positive. -/
+lemma eigenvalues_pos [DecidableEq n] {A : Matrix n n 𝕜}
+    (hA : Matrix.PosDef A) (i : n) : 0 < hA.1.eigenvalues i := by
+  simp only [hA.1.eigenvalues_eq]
+  exact hA.re_dotProduct_pos <| (ofLp_eq_zero 2).ne.2 <|
+    hA.1.eigenvectorBasis.orthonormal.ne_zero i
+
+/-- A Hermitian matrix is positive-definite if and only if its eigenvalues are positive. -/
+lemma _root_.Matrix.IsHermitian.posDef_iff_eigenvalues_pos [DecidableEq n] {A : Matrix n n 𝕜}
+    (hA : A.IsHermitian) : A.PosDef ↔ ∀ i, 0 < hA.eigenvalues i := by
+  refine ⟨fun h => h.eigenvalues_pos, fun h => ?_⟩
+  rw [hA.spectral_theorem]
+  refine (posDef_diagonal_iff.mpr <| by simpa using h).mul_mul_conjTranspose_same ?_
+  rw [vecMul_injective_iff_isUnit, ← Unitary.val_toUnits_apply]
+  exact Units.isUnit _
+
+lemma 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
+  intro i _
+  simpa using hM.eigenvalues_pos i
+
+end PosDef
+end Matrix

Mathlib/LinearAlgebra/Matrix/Spectrum.lean renamed to Mathlib/Analysis/Matrix/Spectrum.lean

@@ -5,7 +5,6 @@ Authors: Adrian Wüthrich
 -/
 import Mathlib.Analysis.Matrix.Order
 import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
-import Mathlib.LinearAlgebra.Matrix.PosDef
 
 /-!
 # Laplacian Matrix

Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

@@ -3,10 +3,8 @@ Copyright (c) 2024 Jon Bannon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Bannon, Jireh Loreaux
 -/
-
-import Mathlib.LinearAlgebra.Matrix.Spectrum
-import Mathlib.LinearAlgebra.Eigenspace.Matrix
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
+import Mathlib.Analysis.Matrix.Spectrum
 import Mathlib.Topology.ContinuousMap.Units
 
 /-!

Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Mohanad Ahmed
 -/
 import Mathlib.Algebra.Order.Ring.Star
-import Mathlib.LinearAlgebra.Matrix.Spectrum
+import Mathlib.LinearAlgebra.Matrix.DotProduct
+import Mathlib.LinearAlgebra.Matrix.Hermitian
 import Mathlib.LinearAlgebra.Matrix.Vec
 import Mathlib.LinearAlgebra.QuadraticForm.Basic
 
@@ -32,6 +33,10 @@ order on matrices on `ℝ` or `ℂ`.
 * `Matrix.PosDef.isUnit`: A positive definite matrix in a field is invertible.
 -/
 
+-- TODO:
+-- assert_not_exists MonoidAlgebra
+assert_not_exists Matrix.IsHermitian.eigenvalues
+
 open WithLp
 
 open scoped ComplexOrder
@@ -178,20 +183,11 @@ protected theorem smul {α : Type*} [CommSemiring α] [PartialOrder α] [StarRin
   simp only [smul_mulVec, dotProduct_smul]
   exact smul_nonneg ha (hx.2 _)
 
-/-- The eigenvalues of a positive semi-definite matrix are non-negative -/
-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 _)]
+lemma diag_nonneg {A : Matrix n n R} (hA : A.PosSemidef) {i : n} : 0 ≤ A i i := by
+  classical simpa [trace] using hA.2 <| Pi.single i 1
 
-theorem det_nonneg [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosSemidef) :
-    0 ≤ M.det := by
-  rw [hM.isHermitian.det_eq_prod_eigenvalues]
-  exact Finset.prod_nonneg fun i _ ↦ by simpa using hM.eigenvalues_nonneg i
+lemma trace_nonneg [AddLeftMono R] {A : Matrix n n R} (hA : A.PosSemidef) : 0 ≤ A.trace :=
+  Fintype.sum_nonneg fun _ ↦ hA.diag_nonneg
 
 end PosSemidef
 
@@ -234,34 +230,6 @@ theorem trace_mul_conjTranspose_self_eq_zero_iff {A : Matrix m n R} :
 
 end trace
 
-lemma eigenvalues_conjTranspose_mul_self_nonneg (A : Matrix m n 𝕜) [DecidableEq n] (i : n) :
-    0 ≤ (isHermitian_conjTranspose_mul_self A).eigenvalues i :=
-  (posSemidef_conjTranspose_mul_self _).eigenvalues_nonneg _
-
-lemma eigenvalues_self_mul_conjTranspose_nonneg (A : Matrix m n 𝕜) [DecidableEq m] (i : m) :
-    0 ≤ (isHermitian_mul_conjTranspose_self A).eigenvalues i :=
-  (posSemidef_self_mul_conjTranspose _).eigenvalues_nonneg _
-
-/-- A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative. -/
-lemma IsHermitian.posSemidef_iff_eigenvalues_nonneg [DecidableEq n] {A : Matrix n n 𝕜}
-    (hA : IsHermitian A) : PosSemidef A ↔ 0 ≤ hA.eigenvalues := by
-  refine ⟨fun h => h.eigenvalues_nonneg, fun h => ?_⟩
-  rw [hA.spectral_theorem]
-  refine (posSemidef_diagonal_iff.mpr ?_).mul_mul_conjTranspose_same _
-  simpa using h
-
-@[deprecated (since := "2025-08-17")] alias ⟨_, IsHermitian.posSemidef_of_eigenvalues_nonneg⟩ :=
-  IsHermitian.posSemidef_iff_eigenvalues_nonneg
-
-theorem PosSemidef.trace_eq_zero_iff {A : Matrix n n 𝕜} (hA : A.PosSemidef) :
-    A.trace = 0 ↔ A = 0 := by
-  refine ⟨fun h => ?_, fun h => h ▸ trace_zero n 𝕜⟩
-  classical
-  simp_rw [hA.isHermitian.trace_eq_sum_eigenvalues, ← RCLike.ofReal_sum,
-    RCLike.ofReal_eq_zero, Finset.sum_eq_zero_iff_of_nonneg (s := Finset.univ)
-      (by simpa using hA.eigenvalues_nonneg), Finset.mem_univ, true_imp_iff] at h
-  exact funext_iff.eq ▸ hA.isHermitian.eigenvalues_eq_zero_iff.mp <| h
-
 section conjugate
 variable [DecidableEq n] {U x : Matrix n n R}
 
@@ -470,32 +438,12 @@ theorem toQuadraticForm' [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) :
     toLinearMap₂'_apply']
   apply hM.2 x hx
 
-/-- The eigenvalues of a positive definite matrix are positive. -/
-lemma eigenvalues_pos [DecidableEq n] {A : Matrix n n 𝕜}
-    (hA : Matrix.PosDef A) (i : n) : 0 < hA.1.eigenvalues i := by
-  simp only [hA.1.eigenvalues_eq]
-  exact hA.re_dotProduct_pos <| (ofLp_eq_zero 2).ne.2 <|
-    hA.1.eigenvectorBasis.orthonormal.ne_zero i
-
-/-- A Hermitian matrix is positive-definite if and only if its eigenvalues are positive. -/
-lemma _root_.Matrix.IsHermitian.posDef_iff_eigenvalues_pos [DecidableEq n] {A : Matrix n n 𝕜}
-    (hA : A.IsHermitian) : A.PosDef ↔ ∀ i, 0 < hA.eigenvalues i := by
-  refine ⟨fun h => h.eigenvalues_pos, fun h => ?_⟩
-  rw [hA.spectral_theorem]
-  refine (posDef_diagonal_iff.mpr <| by simpa using h).mul_mul_conjTranspose_same ?_
-  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
-  intro i _
-  simpa using hM.eigenvalues_pos i
+lemma diag_pos [Nontrivial R] {A : Matrix n n R} (hA : A.PosDef) {i : n} : 0 < A i i := by
+  classical simpa [trace] using hA.2 <| Pi.single i 1
+
+lemma trace_pos [Nontrivial R] [IsOrderedCancelAddMonoid R] [Nonempty n] {A : Matrix n n R}
+    (hA : A.PosDef) : 0 < A.trace :=
+  Finset.sum_pos (fun _ _ ↦ hA.diag_pos) Finset.univ_nonempty
 
 section Field
 variable {K : Type*} [Field K] [PartialOrder K] [StarRing K]