Hermitian matrices over ℝ and ℂ

This file proves that Hermitian matrices over ℝ and ℂ are exactly the ones whose corresponding linear map is self-adjoint.

Tags

self-adjoint matrix, hermitian matrix

theorem Matrix.IsHermitian.coe_re_apply_self {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [RCLike 𝕜] (h : A.IsHermitian) (i : n) : ↑(RCLike.re (A i i)) = A i i

The diagonal elements of a complex Hermitian matrix are real.

theorem Matrix.IsHermitian.coe_re_diag {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [RCLike 𝕜] (h : A.IsHermitian) : (fun (i : n) => ↑(RCLike.re (A.diag i))) = A.diag

The diagonal elements of a complex Hermitian matrix are real.

@[simp]

theorem Matrix.isSymmetric_toLin_iff {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [RCLike 𝕜] [Fintype n] [DecidableEq n] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : OrthonormalBasis n 𝕜 E) : ((toLin b.toBasis b.toBasis) A).IsSymmetric ↔ A.IsHermitian

A matrix is Hermitian iff the corresponding linear map with an orthonormal basis is symmetric.

@[simp]

theorem Matrix.isSymmetric_toEuclideanLin_iff {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [RCLike 𝕜] [Fintype n] [DecidableEq n] : (toEuclideanLin A).IsSymmetric ↔ A.IsHermitian

A matrix is Hermitian iff the corresponding linear map on the Euclidean space is symmetric.

theorem Matrix.IsHermitian.im_star_dotProduct_mulVec_self {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [RCLike 𝕜] [Fintype n] (hA : A.IsHermitian) (x : n → 𝕜) : RCLike.im (star x ⬝ᵥ A.mulVec x) = 0

@[simp]

theorem LinearMap.isHermitian_toMatrix_iff {n : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Fintype n] [DecidableEq n] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {f : E →ₗ[𝕜] E} (b : OrthonormalBasis n 𝕜 E) : ((toMatrix b.toBasis b.toBasis) f).IsHermitian ↔ f.IsSymmetric

A linear map is symmetric iff the corresponding matrix with an orthonormal basis is Hermitian.