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.
Instances For
@[implicit_reducible]
instance
Matrix.instDecidableIsHermitianOfEqConjTranspose
{α : Type u_1}
{n : Type u_4}
[Star α]
(A : Matrix n n α)
[Decidable (A.conjTranspose = A)]
:
Decidable A.IsHermitian
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_iff_isSelfAdjoint
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
:
A.IsHermitian ↔ IsSelfAdjoint A
theorem
IsSelfAdjoint.isHermitian
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
:
IsSelfAdjoint A → A.IsHermitian
Alias of the reverse direction of Matrix.isHermitian_iff_isSelfAdjoint.
theorem
Matrix.IsHermitian.isSelfAdjoint
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
:
A.IsHermitian → IsSelfAdjoint A
Alias of the forward direction of Matrix.isHermitian_iff_isSelfAdjoint.
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 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
@[simp]
theorem
Matrix.isHermitian_map_iff
{α : Type u_1}
{β : Type u_2}
{n : Type u_4}
[Star α]
[Star β]
{A : Matrix n n α}
{f : α → β}
(hf : Function.Semiconj f star star)
(hinj : Function.Injective f)
:
(A.map f).IsHermitian ↔ A.IsHermitian
@[simp]
theorem
Matrix.IsHermitian.of_subsingleton
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
[Subsingleton α]
:
theorem
Matrix.IsHermitian.transpose
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(h : A.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)
:
@[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 : m → n)
:
(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
theorem
Matrix.IsHermitian.reindex
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(h : A.IsHermitian)
(f : n ≃ m)
:
((Matrix.reindex f f) A).IsHermitian
theorem
Matrix.isHermitian_reindex_iff
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(f : n ≃ m)
:
((reindex f f) A).IsHermitian ↔ A.IsHermitian
theorem
Matrix.conjTranspose_comp'
{α : Type u_1}
[Star α]
{I : Type u_5}
{J : Type u_6}
{K : Type u_7}
(M : Matrix I J (Matrix K K α))
:
((comp I J K K α) M).conjTranspose = (comp J I K K α) M.conjTranspose
When the inner matrices are square we can use the induced star operation
theorem
Matrix.isHermitian_comp_iff
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[Star α]
{A : Matrix m m (Matrix n n α)}
:
((comp m m n n α) A).IsHermitian ↔ A.IsHermitian
theorem
Matrix.isHermitian_comp_iff_forall
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[Star α]
{A : Matrix m m (Matrix n n α)}
:
((comp m m n n α) A).IsHermitian ↔ ∀ (i j : m) (i' j' : n), star (A j i j' i') = A i j i' j'
@[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 : A.IsHermitian)
(hBC : B.conjTranspose = C)
(hD : D.IsHermitian)
:
(Matrix.fromBlocks A B C D).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}
[InvolutiveStar α]
{A : Matrix m m α}
{B : Matrix m n α}
{C : Matrix n m α}
{D : Matrix n n α}
:
(fromBlocks A B C D).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}
[AddMonoid α]
[StarAddMonoid α]
[DecidableEq n]
(v : n → α)
(h : IsSelfAdjoint v)
:
(diagonal v).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}
[AddMonoid α]
[StarAddMonoid α]
[DecidableEq n]
{d : n → α}
:
(diagonal d).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}
[AddMonoid α]
[StarAddMonoid α]
[TrivialStar α]
[DecidableEq n]
(v : n → α)
:
(diagonal v).IsHermitian
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 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}
[AddCommMonoid α]
[StarAddMonoid α]
(A : Matrix n n α)
:
(A + A.conjTranspose).IsHermitian
theorem
Matrix.isHermitian_transpose_add_self
{α : Type u_1}
{n : Type u_4}
[AddCommMonoid α]
[StarAddMonoid α]
(A : Matrix n n α)
:
(A.conjTranspose + A).IsHermitian
@[simp]
theorem
Matrix.IsHermitian.neg
{α : Type u_1}
{n : Type u_4}
[AddGroup α]
[StarAddMonoid α]
{A : Matrix n n α}
(h : A.IsHermitian)
:
(-A).IsHermitian
@[simp]
theorem
Matrix.isHermitian_neg_iff
{α : Type u_1}
{n : Type u_4}
[AddGroup α]
[StarAddMonoid α]
{A : Matrix n n α}
:
(-A).IsHermitian ↔ A.IsHermitian
@[simp]
theorem
Matrix.IsHermitian.sub
{α : Type u_1}
{n : Type u_4}
[AddGroup α]
[StarAddMonoid α]
{A B : Matrix n n α}
(hA : A.IsHermitian)
(hB : B.IsHermitian)
:
(A - B).IsHermitian
theorem
Matrix.IsHermitian.smul
{α : Type u_1}
{n : Type u_4}
{R : Type u_5}
[Star R]
[Star α]
[SMul R α]
[StarModule R α]
{A : Matrix n n α}
(h : A.IsHermitian)
{k : R}
(hk : IsSelfAdjoint k)
:
(k • A).IsHermitian
theorem
Matrix.IsHermitian.of_smul
{α : Type u_1}
{n : Type u_4}
{R : Type u_5}
[Monoid R]
[Star R]
[Star α]
[MulAction R α]
[StarModule R α]
{A : Matrix n n α}
{k : R}
[Invertible k]
(h : (k • A).IsHermitian)
(hk : IsSelfAdjoint k)
:
theorem
Matrix.IsHermitian.of_smul'
{α : Type u_1}
{n : Type u_4}
{R : Type u_5}
[Monoid R]
[Star R]
[Star α]
[MulAction R α]
[StarModule R α]
{A : Matrix n n α}
{k : R}
[Invertible k]
(h : (k • A).IsHermitian)
(hk : IsSelfAdjoint ⅟k)
:
Assumes IsSelfAdjoint ⅟k instead of IsSelfAdjoint k.
These are equivalent given StarMul R
@[simp]
theorem
Matrix.isHermitian_smul_iff
{α : Type u_1}
{n : Type u_4}
{R : Type u_5}
[Monoid R]
[Star R]
[Star α]
[MulAction R α]
[StarModule R α]
{A : Matrix n n α}
{k : R}
[Invertible k]
(hk : IsSelfAdjoint k)
:
(k • A).IsHermitian ↔ A.IsHermitian
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 α)
:
(A * A.conjTranspose).IsHermitian
Note this is more general than IsSelfAdjoint.mul_star_self as B can be rectangular.
theorem
Matrix.isHermitian_conjTranspose_mul_self
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[NonUnitalSemiring α]
[StarRing α]
[Fintype m]
(A : Matrix m n α)
:
(A.conjTranspose * A).IsHermitian
Note this is more general than IsSelfAdjoint.star_mul_self as B can be rectangular.
@[deprecated Matrix.isHermitian_conjTranspose_mul_self (since := "2025-11-10")]
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 α)
:
(A.conjTranspose * A).IsHermitian
Alias of Matrix.isHermitian_conjTranspose_mul_self.
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 : 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}
[NonUnitalSemiring α]
[StarRing α]
[Fintype m]
{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.IsHermitian.commute_iff
{α : Type u_1}
{n : Type u_4}
[NonUnitalSemiring α]
[StarRing α]
[Fintype n]
{A 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}
[NonAssocSemiring α]
[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).
@[simp]
theorem
Matrix.isHermitian_natCast
{α : Type u_1}
{n : Type u_4}
[Semiring α]
[StarRing α]
[DecidableEq n]
(d : ℕ)
:
(↑d).IsHermitian
theorem
Matrix.IsHermitian.pow
{α : Type u_1}
{n : Type u_4}
[Semiring α]
[StarRing α]
[Fintype n]
[DecidableEq n]
{A : Matrix n n α}
(h : A.IsHermitian)
(k : ℕ)
:
(A ^ k).IsHermitian
@[simp]
theorem
Matrix.isHermitian_intCast
{α : Type u_1}
{n : Type u_4}
[Ring α]
[StarRing α]
[DecidableEq n]
(d : ℤ)
:
(↑d).IsHermitian
theorem
Matrix.IsHermitian.inv
{α : Type u_1}
{m : Type u_3}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
{A : Matrix m m α}
(hA : A.IsHermitian)
:
@[simp]
theorem
Matrix.isHermitian_inv
{α : Type u_1}
{m : Type u_3}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
(A : Matrix m m α)
[Invertible A]
:
A⁻¹.IsHermitian ↔ A.IsHermitian
theorem
Matrix.IsHermitian.adjugate
{α : Type u_1}
{m : Type u_3}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
{A : Matrix m m α}
(hA : A.IsHermitian)
:
theorem
Matrix.IsHermitian.zpow
{α : Type u_1}
{m : Type u_3}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
{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.
Notation for Sum.elim, scoped within the Matrix namespace.
Instances For
theorem
Matrix.schur_complement_eq₁₁
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
[Fintype n]
{A : Matrix m m α}
(B : Matrix m n α)
(D : Matrix n n α)
(x : m → α)
(y : n → α)
[Invertible A]
(hA : A.IsHermitian)
:
theorem
Matrix.schur_complement_eq₂₂
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[CommRing α]
[StarRing α]
[Fintype m]
[Fintype n]
[DecidableEq n]
(A : Matrix m m α)
(B : Matrix m n α)
{D : Matrix n n α}
(x : m → α)
(y : n → α)
[Invertible D]
(hD : D.IsHermitian)
:
vecMul (star (Sum.elim x y)) (fromBlocks A B B.conjTranspose D) ⬝ᵥ Sum.elim x y = vecMul (star ((D⁻¹ * B.conjTranspose).mulVec x + y)) D ⬝ᵥ ((D⁻¹ * B.conjTranspose).mulVec x + y) + vecMul (star x) (A - B * D⁻¹ * B.conjTranspose) ⬝ᵥ x
theorem
Matrix.IsHermitian.fromBlocks₁₁
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[CommRing α]
[StarRing α]
[Fintype m]
[DecidableEq m]
{A : Matrix m m α}
(B : Matrix m n α)
(D : Matrix n n α)
(hA : A.IsHermitian)
:
(Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (D - B.conjTranspose * A⁻¹ * B).IsHermitian
theorem
Matrix.IsHermitian.fromBlocks₂₂
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[CommRing α]
[StarRing α]
[Fintype n]
[DecidableEq n]
(A : Matrix m m α)
(B : Matrix m n α)
{D : Matrix n n α}
(hD : D.IsHermitian)
:
(Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (A - B * D⁻¹ * B.conjTranspose).IsHermitian