# Hermitian matrices #

This file defines hermitian matrices and some basic results about them.

See also IsSelfAdjoint, which generalizes this definition to other star rings.

## Main definition #

• Matrix.IsHermitian : a matrix A : Matrix n n α is hermitian if Aᴴ = A.

## Tags #

def Matrix.IsHermitian {α : Type u_1} {n : Type u_4} [Star α] (A : Matrix n n α) :

A matrix is hermitian if it is equal to its conjugate transpose. On the reals, this definition captures symmetric matrices.

Equations
• A.IsHermitian = (A.conjTranspose = A)
Instances For
instance Matrix.instDecidableIsHermitianOfEqConjTranspose {α : Type u_1} {n : Type u_4} [Star α] (A : Matrix n n α) [Decidable (A.conjTranspose = A)] :
Decidable A.IsHermitian
Equations
theorem Matrix.IsHermitian.eq {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) :
A.conjTranspose = A
theorem Matrix.IsHermitian.isSelfAdjoint {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) :
theorem Matrix.IsHermitian.ext {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} :
(∀ (i j : n), star (A j i) = A i j)A.IsHermitian
theorem Matrix.IsHermitian.apply {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) (i : n) (j : n) :
star (A j i) = A i j
theorem Matrix.IsHermitian.ext_iff {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} :
A.IsHermitian ∀ (i j : n), star (A j i) = A i j
@[simp]
theorem Matrix.IsHermitian.map {α : Type u_1} {β : Type u_2} {n : Type u_4} [Star α] [Star β] {A : Matrix n n α} (h : A.IsHermitian) (f : αβ) (hf : Function.Semiconj f star star) :
(A.map f).IsHermitian
theorem Matrix.IsHermitian.transpose {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) :
A.transpose.IsHermitian
@[simp]
theorem Matrix.isHermitian_transpose_iff {α : Type u_1} {n : Type u_4} [Star α] (A : Matrix n n α) :
A.transpose.IsHermitian A.IsHermitian
theorem Matrix.IsHermitian.conjTranspose {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) :
A.conjTranspose.IsHermitian
@[simp]
theorem Matrix.IsHermitian.submatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) (f : mn) :
(A.submatrix f f).IsHermitian
@[simp]
theorem Matrix.isHermitian_submatrix_equiv {α : Type u_1} {m : Type u_3} {n : Type u_4} [Star α] {A : Matrix n n α} (e : m n) :
(A.submatrix e e).IsHermitian A.IsHermitian
@[simp]
theorem Matrix.isHermitian_conjTranspose_iff {α : Type u_1} {n : Type u_4} [] (A : Matrix n n α) :
A.conjTranspose.IsHermitian A.IsHermitian
theorem Matrix.IsHermitian.fromBlocks {α : Type u_1} {m : Type u_3} {n : Type u_4} [] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} (hA : A.IsHermitian) (hBC : B.conjTranspose = C) (hD : D.IsHermitian) :
().IsHermitian

A block matrix A.from_blocks B C D is hermitian, if A and D are hermitian and Bᴴ = C.

theorem Matrix.isHermitian_fromBlocks_iff {α : Type u_1} {m : Type u_3} {n : Type u_4} [] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} :
().IsHermitian A.IsHermitian B.conjTranspose = C C.conjTranspose = B D.IsHermitian

This is the iff version of Matrix.IsHermitian.fromBlocks.

theorem Matrix.isHermitian_diagonal_of_self_adjoint {α : Type u_1} {n : Type u_4} [] [] [] (v : nα) (h : ) :
().IsHermitian

A diagonal matrix is hermitian if the entries are self-adjoint (as a vector)

theorem Matrix.isHermitian_diagonal_iff {α : Type u_1} {n : Type u_4} [] [] [] {d : nα} :
().IsHermitian ∀ (i : n), IsSelfAdjoint (d i)

A diagonal matrix is hermitian if each diagonal entry is self-adjoint

@[simp]
theorem Matrix.isHermitian_diagonal {α : Type u_1} {n : Type u_4} [] [] [] [] (v : nα) :
().IsHermitian

A diagonal matrix is hermitian if the entries have the trivial star operation (such as on the reals).

@[simp]
theorem Matrix.isHermitian_zero {α : Type u_1} {n : Type u_4} [] [] :
@[simp]
theorem Matrix.IsHermitian.add {α : Type u_1} {n : Type u_4} [] [] {A : Matrix n n α} {B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) :
(A + B).IsHermitian
theorem Matrix.isHermitian_add_transpose_self {α : Type u_1} {n : Type u_4} [] [] (A : Matrix n n α) :
(A + A.conjTranspose).IsHermitian
theorem Matrix.isHermitian_transpose_add_self {α : Type u_1} {n : Type u_4} [] [] (A : Matrix n n α) :
(A.conjTranspose + A).IsHermitian
@[simp]
theorem Matrix.IsHermitian.neg {α : Type u_1} {n : Type u_4} [] [] {A : Matrix n n α} (h : A.IsHermitian) :
(-A).IsHermitian
@[simp]
theorem Matrix.IsHermitian.sub {α : Type u_1} {n : Type u_4} [] [] {A : Matrix n n α} {B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) :
(A - B).IsHermitian
theorem Matrix.isHermitian_mul_conjTranspose_self {α : Type u_1} {m : Type u_3} {n : Type u_4} [] [] (A : Matrix m n α) :
(A * A.conjTranspose).IsHermitian

Note this is more general than IsSelfAdjoint.mul_star_self as B can be rectangular.

theorem Matrix.isHermitian_transpose_mul_self {α : Type u_1} {m : Type u_3} {n : Type u_4} [] [] (A : Matrix m n α) :
(A.conjTranspose * A).IsHermitian

Note this is more general than IsSelfAdjoint.star_mul_self as B can be rectangular.

theorem Matrix.isHermitian_conjTranspose_mul_mul {α : Type u_1} {m : Type u_3} {n : Type u_4} [] [] {A : Matrix m m α} (B : Matrix m n α) (hA : A.IsHermitian) :
(B.conjTranspose * A * B).IsHermitian

Note this is more general than IsSelfAdjoint.conjugate' as B can be rectangular.

theorem Matrix.isHermitian_mul_mul_conjTranspose {α : Type u_1} {m : Type u_3} {n : Type u_4} [] [] {A : Matrix m m α} (B : Matrix n m α) (hA : A.IsHermitian) :
(B * A * B.conjTranspose).IsHermitian

Note this is more general than IsSelfAdjoint.conjugate as B can be rectangular.

theorem Matrix.commute_iff {α : Type u_1} {n : Type u_4} [] [] {A : Matrix n n α} {B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) :
Commute A B (A * B).IsHermitian
@[simp]
theorem Matrix.isHermitian_one {α : Type u_1} {n : Type u_4} [] [] [] :

Note this is more general for matrices than isSelfAdjoint_one as it does not require Fintype n, which is necessary for Monoid (Matrix n n R).

theorem Matrix.IsHermitian.pow {α : Type u_1} {n : Type u_4} [] [] [] [] {A : Matrix n n α} (h : A.IsHermitian) (k : ) :
(A ^ k).IsHermitian
theorem Matrix.IsHermitian.inv {α : Type u_1} {m : Type u_3} [] [] [] [] {A : Matrix m m α} (hA : A.IsHermitian) :
A⁻¹.IsHermitian
@[simp]
theorem Matrix.isHermitian_inv {α : Type u_1} {m : Type u_3} [] [] [] [] (A : Matrix m m α) [] :
A⁻¹.IsHermitian A.IsHermitian
theorem Matrix.IsHermitian.adjugate {α : Type u_1} {m : Type u_3} [] [] [] [] {A : Matrix m m α} (hA : A.IsHermitian) :
theorem Matrix.IsHermitian.zpow {α : Type u_1} {m : Type u_3} [] [] [] [] {A : Matrix m m α} (h : A.IsHermitian) (k : ) :
(A ^ k).IsHermitian

Note that IsSelfAdjoint.zpow does not apply to matrices as they are not a division ring.

theorem Matrix.IsHermitian.coe_re_apply_self {α : Type u_1} {n : Type u_4} [] {A : Matrix n n α} (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_4} [] {A : Matrix n n α} (h : A.IsHermitian) :
(fun (i : n) => (RCLike.re (A.diag i))) = A.diag

The diagonal elements of a complex hermitian matrix are real.

theorem Matrix.isHermitian_iff_isSymmetric {α : Type u_1} {n : Type u_4} [] [] [] {A : Matrix n n α} :
A.IsHermitian (Matrix.toEuclideanLin A).IsSymmetric

A matrix is hermitian iff the corresponding linear map is self adjoint.