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 matrixA : Matrix n n αis hermitian ifAᴴ = A.
Tags #
self-adjoint matrix, hermitian matrix
A matrix is hermitian if it is equal to its conjugate transpose. On the reals, this definition captures symmetric matrices.
Equations
- Matrix.IsHermitian A = (Matrix.conjTranspose A = A)
Instances For
theorem
Matrix.IsHermitian.eq
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
:
theorem
Matrix.IsHermitian.isSelfAdjoint
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
:
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) → Matrix.IsHermitian A
theorem
Matrix.IsHermitian.apply
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
(i : n)
(j : n)
:
theorem
Matrix.IsHermitian.ext_iff
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
:
Matrix.IsHermitian A ↔ ∀ (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 : Matrix.IsHermitian A)
(f : α → β)
(hf : Function.Semiconj f star star)
:
Matrix.IsHermitian (Matrix.map A f)
theorem
Matrix.IsHermitian.transpose
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
:
@[simp]
theorem
Matrix.isHermitian_transpose_iff
{α : Type u_1}
{n : Type u_4}
[Star α]
(A : Matrix n n α)
:
theorem
Matrix.IsHermitian.conjTranspose
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
:
@[simp]
theorem
Matrix.IsHermitian.submatrix
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
(f : m → n)
:
Matrix.IsHermitian (Matrix.submatrix A f f)
@[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)
:
Matrix.IsHermitian (Matrix.submatrix A ⇑e ⇑e) ↔ Matrix.IsHermitian A
@[simp]
theorem
Matrix.isHermitian_conjTranspose_iff
{α : Type u_1}
{n : Type u_4}
[InvolutiveStar α]
(A : Matrix n n α)
:
theorem
Matrix.IsHermitian.fromBlocks
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[InvolutiveStar α]
{A : Matrix m m α}
{B : Matrix m n α}
{C : Matrix n m α}
{D : Matrix n n α}
(hA : Matrix.IsHermitian A)
(hBC : Matrix.conjTranspose B = C)
(hD : Matrix.IsHermitian D)
:
Matrix.IsHermitian (Matrix.fromBlocks A B C D)
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}
[InvolutiveStar α]
{A : Matrix m m α}
{B : Matrix m n α}
{C : Matrix n m α}
{D : Matrix n n α}
:
Matrix.IsHermitian (Matrix.fromBlocks A B C D) ↔ Matrix.IsHermitian A ∧ Matrix.conjTranspose B = C ∧ Matrix.conjTranspose C = B ∧ Matrix.IsHermitian D
This is the iff version of Matrix.IsHermitian.fromBlocks.
theorem
Matrix.isHermitian_diagonal_of_self_adjoint
{α : Type u_1}
{n : Type u_4}
[AddMonoid α]
[StarAddMonoid α]
[DecidableEq n]
(v : n → α)
(h : IsSelfAdjoint v)
:
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}
[AddMonoid α]
[StarAddMonoid α]
[DecidableEq n]
{d : n → α}
:
Matrix.IsHermitian (Matrix.diagonal d) ↔ ∀ (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}
[AddMonoid α]
[StarAddMonoid α]
[TrivialStar α]
[DecidableEq n]
(v : n → α)
:
A diagonal matrix is hermitian if the entries have the trivial star operation
(such as on the reals).
@[simp]
@[simp]
theorem
Matrix.IsHermitian.add
{α : Type u_1}
{n : Type u_4}
[AddMonoid α]
[StarAddMonoid α]
{A : Matrix n n α}
{B : Matrix n n α}
(hA : Matrix.IsHermitian A)
(hB : Matrix.IsHermitian B)
:
Matrix.IsHermitian (A + B)
theorem
Matrix.isHermitian_add_transpose_self
{α : Type u_1}
{n : Type u_4}
[AddCommMonoid α]
[StarAddMonoid α]
(A : Matrix n n α)
:
theorem
Matrix.isHermitian_transpose_add_self
{α : Type u_1}
{n : Type u_4}
[AddCommMonoid α]
[StarAddMonoid α]
(A : Matrix n n α)
:
@[simp]
theorem
Matrix.IsHermitian.neg
{α : Type u_1}
{n : Type u_4}
[AddGroup α]
[StarAddMonoid α]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
:
@[simp]
theorem
Matrix.IsHermitian.sub
{α : Type u_1}
{n : Type u_4}
[AddGroup α]
[StarAddMonoid α]
{A : Matrix n n α}
{B : Matrix n n α}
(hA : Matrix.IsHermitian A)
(hB : Matrix.IsHermitian B)
:
Matrix.IsHermitian (A - B)
theorem
Matrix.isHermitian_mul_conjTranspose_self
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[NonUnitalSemiring α]
[StarRing α]
[Fintype n]
(A : Matrix m n α)
:
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}
[NonUnitalSemiring α]
[StarRing α]
[Fintype m]
(A : Matrix m n α)
:
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}
[NonUnitalSemiring α]
[StarRing α]
[Fintype m]
{A : Matrix m m α}
(B : Matrix m n α)
(hA : Matrix.IsHermitian A)
:
Matrix.IsHermitian (Matrix.conjTranspose B * A * B)
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}
[NonUnitalSemiring α]
[StarRing α]
[Fintype m]
{A : Matrix m m α}
(B : Matrix n m α)
(hA : Matrix.IsHermitian A)
:
Matrix.IsHermitian (B * A * Matrix.conjTranspose B)
Note this is more general than IsSelfAdjoint.conjugate as B can be rectangular.
theorem
Matrix.commute_iff
{α : Type u_1}
{n : Type u_4}
[NonUnitalSemiring α]
[StarRing α]
[Fintype n]
{A : Matrix n n α}
{B : Matrix n n α}
(hA : Matrix.IsHermitian A)
(hB : Matrix.IsHermitian B)
:
Commute A B ↔ Matrix.IsHermitian (A * B)
@[simp]
theorem
Matrix.isHermitian_one
{α : Type u_1}
{n : Type u_4}
[Semiring α]
[StarRing α]
[DecidableEq n]
:
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}
[Semiring α]
[StarRing α]
[Fintype n]
[DecidableEq n]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
(k : ℕ)
:
Matrix.IsHermitian (A ^ k)
theorem
Matrix.IsHermitian.inv
{α : Type u_1}
{m : Type u_3}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
{A : Matrix m m α}
(hA : Matrix.IsHermitian A)
:
@[simp]
theorem
Matrix.isHermitian_inv
{α : Type u_1}
{m : Type u_3}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
(A : Matrix m m α)
[Invertible A]
:
theorem
Matrix.IsHermitian.adjugate
{α : Type u_1}
{m : Type u_3}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
{A : Matrix m m α}
(hA : Matrix.IsHermitian A)
:
theorem
Matrix.IsHermitian.zpow
{α : Type u_1}
{m : Type u_3}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
{A : Matrix m m α}
(h : Matrix.IsHermitian A)
(k : ℤ)
:
Matrix.IsHermitian (A ^ k)
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}
[IsROrC α]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
(i : n)
:
↑(IsROrC.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}
[IsROrC α]
{A : Matrix n n α}
(h : Matrix.IsHermitian A)
:
(fun (i : n) => ↑(IsROrC.re (Matrix.diag A i))) = Matrix.diag A
The diagonal elements of a complex hermitian matrix are real.
theorem
Matrix.isHermitian_iff_isSymmetric
{α : Type u_1}
{n : Type u_4}
[IsROrC α]
[Fintype n]
[DecidableEq n]
{A : Matrix n n α}
:
Matrix.IsHermitian A ↔ LinearMap.IsSymmetric (Matrix.toEuclideanLin A)
A matrix is hermitian iff the corresponding linear map is self adjoint.