feat(Analysis/Hermitian): more lemma to convert between IsHermitian and IsSymmetric

Author: wwylele

Mathlib/Analysis/InnerProductSpace/Positive.lean

@@ -202,7 +202,7 @@ theorem isPositive_linearIsometryEquiv_conj_iff {T : E →ₗ[𝕜] E} (f : E 
 /-- `A.toEuclideanLin` is positive if and only if `A` is positive semi-definite. -/
 @[simp] theorem _root_.Matrix.isPositive_toEuclideanLin_iff {n : Type*} [Fintype n] [DecidableEq n]
     {A : Matrix n n 𝕜} : A.toEuclideanLin.IsPositive ↔ A.PosSemidef := by
-  simp_rw [LinearMap.IsPositive, ← Matrix.isHermitian_iff_isSymmetric, inner_re_symm,
+  simp_rw [LinearMap.IsPositive, Matrix.isSymmetric_toEuclideanLin_iff, inner_re_symm,
     EuclideanSpace.inner_eq_star_dotProduct, Matrix.ofLp_toLpLin, Matrix.toLin'_apply,
     dotProduct_comm (A.mulVec _), Matrix.posSemidef_iff_dotProduct_mulVec, and_congr_right_iff,
     RCLike.nonneg_iff (K := 𝕜)]

Mathlib/Analysis/Matrix/Hermitian.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.InnerProductSpace.PiL2
 public import Mathlib.LinearAlgebra.Matrix.Hermitian
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 
 /-!
 # Hermitian matrices over ℝ and ℂ
@@ -38,22 +39,39 @@ lemma IsHermitian.coe_re_apply_self (h : A.IsHermitian) (i : n) : (re (A i i) :
 lemma IsHermitian.coe_re_diag (h : A.IsHermitian) : (fun i => (re (A.diag i) : 𝕜)) = A.diag :=
   funext h.coe_re_apply_self
 
-/-- A matrix is Hermitian iff the corresponding linear map is self adjoint. -/
+/-- A matrix is Hermitian iff the corresponding linear map with an orthonormal basis is self
+adjoint. -/
+@[simp]
+lemma isSymmetric_toLin_iff [Fintype n] [DecidableEq n] {E : Type*}
+    [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : OrthonormalBasis n 𝕜 E) :
+    (A.toLin b.toBasis b.toBasis).IsSymmetric ↔ A.IsHermitian := by
+  have : FiniteDimensional 𝕜 E := b.toBasis.finiteDimensional_of_finite
+  simp_rw [LinearMap.IsSymmetric, ← LinearMap.adjoint_inner_left, ← toLin_conjTranspose]
+  refine ⟨fun h ↦ ?_, fun h _ _ ↦ by rw [h.eq]⟩
+  simpa using (LinearMap.ext fun x ↦ ext_inner_right _ (h x)).symm
+
+/-- A matrix is Hermitian iff the corresponding linear map on the Euclidean space is self adjoint.
+-/
+@[simp]
+lemma isSymmetric_toEuclideanLin_iff [Fintype n] [DecidableEq n] :
+    A.toEuclideanLin.IsSymmetric ↔ A.IsHermitian :=
+  isSymmetric_toLin_iff (EuclideanSpace.basisFun n 𝕜)
+
+@[deprecated isSymmetric_toEuclideanLin_iff (since := "2026-03-30")]
 lemma isHermitian_iff_isSymmetric [Fintype n] [DecidableEq n] :
-    IsHermitian A ↔ A.toEuclideanLin.IsSymmetric := by
-  rw [LinearMap.IsSymmetric, (WithLp.toLp_surjective _).forall₂]
-  simp only [toLpLin_toLp, Matrix.toLin'_apply, EuclideanSpace.inner_eq_star_dotProduct,
-    star_mulVec]
-  constructor
-  · rintro (h : Aᴴ = A) x y
-    rw [dotProduct_comm, ← dotProduct_mulVec, h, dotProduct_comm]
-  · intro h
-    ext i j
-    simpa [(Pi.single_star i 1).symm] using h (Pi.single i 1) (Pi.single j 1)
+    IsHermitian A ↔ A.toEuclideanLin.IsSymmetric := isSymmetric_toEuclideanLin_iff.symm
 
 lemma IsHermitian.im_star_dotProduct_mulVec_self [Fintype n] (hA : A.IsHermitian) (x : n → 𝕜) :
      RCLike.im (star x ⬝ᵥ A *ᵥ x) = 0 := by
   classical
-  simpa [dotProduct_comm] using (isHermitian_iff_isSymmetric.mp hA).im_inner_self_apply _
+  simpa [dotProduct_comm] using (isSymmetric_toEuclideanLin_iff.mpr hA).im_inner_self_apply _
 
 end Matrix
+
+/-- A linear map is self adjoint if the corresponding matrix with an orthonormal basis is Hermitian.
+-/
+@[simp]
+lemma LinearMap.isHermitian_toMatrix_iff {n 𝕜 E : Type*} [Fintype n] [DecidableEq n] [RCLike 𝕜]
+    [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {f : E →ₗ[𝕜] E} (b : OrthonormalBasis n 𝕜 E) :
+    (f.toMatrix b.toBasis b.toBasis).IsHermitian ↔ f.IsSymmetric := by
+  rw [← Matrix.isSymmetric_toLin_iff b, Matrix.toLin_toMatrix]

Mathlib/Analysis/Matrix/Spectrum.lean

@@ -56,7 +56,7 @@ variable (hA : A.IsHermitian) (hB : B.IsHermitian)
 /-- The eigenvalues of a Hermitian matrix, indexed by `Fin (Fintype.card n)` where `n` is the index
 type of the matrix. -/
 noncomputable def eigenvalues₀ : Fin (Fintype.card n) → ℝ :=
-  (isHermitian_iff_isSymmetric.1 hA).eigenvalues finrank_euclideanSpace
+  (isSymmetric_toEuclideanLin_iff.mpr hA).eigenvalues finrank_euclideanSpace
 
 lemma eigenvalues₀_antitone : Antitone hA.eigenvalues₀ :=
   LinearMap.IsSymmetric.eigenvalues_antitone ..
@@ -67,14 +67,14 @@ noncomputable def eigenvalues : n → ℝ := fun i =>
 
 /-- A choice of an orthonormal basis of eigenvectors of a Hermitian matrix. -/
 noncomputable def eigenvectorBasis : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n) :=
-  ((isHermitian_iff_isSymmetric.1 hA).eigenvectorBasis finrank_euclideanSpace).reindex
+  ((isSymmetric_toEuclideanLin_iff.mpr hA).eigenvectorBasis finrank_euclideanSpace).reindex
     (Fintype.equivOfCardEq (Fintype.card_fin _))
 
 lemma mulVec_eigenvectorBasis (j : n) :
     A *ᵥ ⇑(hA.eigenvectorBasis j) = (hA.eigenvalues j) • ⇑(hA.eigenvectorBasis j) := by
   simpa only [eigenvectorBasis, OrthonormalBasis.reindex_apply, toLpLin_apply,
     RCLike.real_smul_eq_coe_smul (K := 𝕜)] using
-      congr(⇑$((isHermitian_iff_isSymmetric.1 hA).apply_eigenvectorBasis
+      congr(⇑$((isSymmetric_toEuclideanLin_iff.mpr hA).apply_eigenvectorBasis
         finrank_euclideanSpace ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm j)))
 
 /-- Eigenvalues of a Hermitian matrix A are in the ℝ spectrum of A. -/