From 8cf5f675ea6acaf8966061c2ed5584429750d76b Mon Sep 17 00:00:00 2001 From: Weiyi Wang Date: Sat, 28 Mar 2026 21:10:10 -0400 Subject: [PATCH 1/6] feat(Analysis/Hermitian): more lemma to convert between IsHermitian and IsSymmetric --- .../Analysis/InnerProductSpace/Positive.lean | 2 +- Mathlib/Analysis/Matrix/Hermitian.lean | 42 +++++++++++++------ Mathlib/Analysis/Matrix/Spectrum.lean | 6 +-- 3 files changed, 34 insertions(+), 16 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index b82d0ce8216dd6..4112b4b8bb62a1 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/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 := π•œ)] diff --git a/Mathlib/Analysis/Matrix/Hermitian.lean b/Mathlib/Analysis/Matrix/Hermitian.lean index ecd098cc32aede..8e8fd9ef0c48aa 100644 --- a/Mathlib/Analysis/Matrix/Hermitian.lean +++ b/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 iff 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] diff --git a/Mathlib/Analysis/Matrix/Spectrum.lean b/Mathlib/Analysis/Matrix/Spectrum.lean index 1e6809ddfb7d49..a9b64713c1e593 100644 --- a/Mathlib/Analysis/Matrix/Spectrum.lean +++ b/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. -/ From e45d0bc491273b683e0319eca1e4f9c047a803eb Mon Sep 17 00:00:00 2001 From: Weiyi Wang Date: Tue, 31 Mar 2026 07:40:04 -0400 Subject: [PATCH 2/6] Update Mathlib/Analysis/Matrix/Hermitian.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/Matrix/Hermitian.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Matrix/Hermitian.lean b/Mathlib/Analysis/Matrix/Hermitian.lean index 8e8fd9ef0c48aa..99490cb437099e 100644 --- a/Mathlib/Analysis/Matrix/Hermitian.lean +++ b/Mathlib/Analysis/Matrix/Hermitian.lean @@ -57,7 +57,8 @@ 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")] +@[deprecated isSymmetric_toEuclideanLin_iff "use isSymmetric_toEuclideanLin_iff.symm" + (since := "2026-03-30")] lemma isHermitian_iff_isSymmetric [Fintype n] [DecidableEq n] : IsHermitian A ↔ A.toEuclideanLin.IsSymmetric := isSymmetric_toEuclideanLin_iff.symm From 6f5cbd1c18efc0bb94fa2ee4f05d9d6b69e0c764 Mon Sep 17 00:00:00 2001 From: Weiyi Wang Date: Tue, 31 Mar 2026 07:40:15 -0400 Subject: [PATCH 3/6] Update Mathlib/Analysis/Matrix/Hermitian.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/Matrix/Hermitian.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Matrix/Hermitian.lean b/Mathlib/Analysis/Matrix/Hermitian.lean index 99490cb437099e..526b8209ef5710 100644 --- a/Mathlib/Analysis/Matrix/Hermitian.lean +++ b/Mathlib/Analysis/Matrix/Hermitian.lean @@ -50,8 +50,8 @@ lemma isSymmetric_toLin_iff [Fintype n] [DecidableEq n] {E : Type*} 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. --/ +/-- 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 := From e8dcfa9b2b905152df33388c02e216dd743f1506 Mon Sep 17 00:00:00 2001 From: Weiyi Wang Date: Tue, 31 Mar 2026 19:06:12 -0400 Subject: [PATCH 4/6] Update Mathlib/Analysis/Matrix/Hermitian.lean Co-authored-by: Jireh Loreaux --- Mathlib/Analysis/Matrix/Hermitian.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Matrix/Hermitian.lean b/Mathlib/Analysis/Matrix/Hermitian.lean index 526b8209ef5710..ff0fc395761c80 100644 --- a/Mathlib/Analysis/Matrix/Hermitian.lean +++ b/Mathlib/Analysis/Matrix/Hermitian.lean @@ -39,8 +39,8 @@ 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 with an orthonormal basis is self -adjoint. -/ +/-- A matrix is Hermitian iff the corresponding linear map with an orthonormal basis is +symmetric. -/ @[simp] lemma isSymmetric_toLin_iff [Fintype n] [DecidableEq n] {E : Type*} [NormedAddCommGroup E] [InnerProductSpace π•œ E] (b : OrthonormalBasis n π•œ E) : From b8c4c365f55da9332f587e1d955550ad5ca3efcb Mon Sep 17 00:00:00 2001 From: Weiyi Wang Date: Tue, 31 Mar 2026 19:06:19 -0400 Subject: [PATCH 5/6] Update Mathlib/Analysis/Matrix/Hermitian.lean Co-authored-by: Jireh Loreaux --- Mathlib/Analysis/Matrix/Hermitian.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Matrix/Hermitian.lean b/Mathlib/Analysis/Matrix/Hermitian.lean index ff0fc395761c80..07a1ccea1e06aa 100644 --- a/Mathlib/Analysis/Matrix/Hermitian.lean +++ b/Mathlib/Analysis/Matrix/Hermitian.lean @@ -50,8 +50,8 @@ lemma isSymmetric_toLin_iff [Fintype n] [DecidableEq n] {E : Type*} 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. -/ +/-- A matrix is Hermitian iff the corresponding linear map on the Euclidean space is +symmetric. -/ @[simp] lemma isSymmetric_toEuclideanLin_iff [Fintype n] [DecidableEq n] : A.toEuclideanLin.IsSymmetric ↔ A.IsHermitian := From 82c74379bd7f6d915af34ef1c829f3e40880da52 Mon Sep 17 00:00:00 2001 From: Weiyi Wang Date: Tue, 31 Mar 2026 19:06:26 -0400 Subject: [PATCH 6/6] Update Mathlib/Analysis/Matrix/Hermitian.lean Co-authored-by: Jireh Loreaux --- Mathlib/Analysis/Matrix/Hermitian.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Matrix/Hermitian.lean b/Mathlib/Analysis/Matrix/Hermitian.lean index 07a1ccea1e06aa..3ab2eaec573076 100644 --- a/Mathlib/Analysis/Matrix/Hermitian.lean +++ b/Mathlib/Analysis/Matrix/Hermitian.lean @@ -69,7 +69,7 @@ lemma IsHermitian.im_star_dotProduct_mulVec_self [Fintype n] (hA : A.IsHermitian end Matrix -/-- A linear map is self adjoint iff the corresponding matrix with an orthonormal basis is +/-- A linear map is symmetric iff the corresponding matrix with an orthonormal basis is Hermitian. -/ @[simp] lemma LinearMap.isHermitian_toMatrix_iff {n π•œ E : Type*} [Fintype n] [DecidableEq n] [RCLike π•œ]