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
- 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)]
:
Equations
theorem
Matrix.IsHermitian.eq
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
(h : A.IsHermitian)
:
theorem
Matrix.isHermitian_iff_isSelfAdjoint
{α : Type u_1}
{n : Type u_4}
[Star α]
{A : Matrix n n α}
:
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)
:
@[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)
:
@[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 : 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_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 → α}
:
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.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_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_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
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)
:
@[deprecated Matrix.IsHermitian.commute_iff (since := "13-08-2025")]
theorem
Matrix.commute_iff
{α : Type u_1}
{n : Type u_4}
[NonUnitalSemiring α]
[StarRing α]
[Fintype n]
{A B : Matrix n n α}
(hA : A.IsHermitian)
(hB : B.IsHermitian)
:
Alias of Matrix.IsHermitian.commute_iff.
@[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).
@[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]
:
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.
Equations
- Matrix.«term_⊕ᵥ_» = Lean.ParserDescr.trailingNode `Matrix.«term_⊕ᵥ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ᵥ ") (Lean.ParserDescr.cat `term 66))
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)
:
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)
:
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)
:
theorem
Matrix.IsHermitian.coe_re_apply_self
{α : Type u_1}
{n : Type u_4}
[RCLike α]
{A : Matrix n n α}
(h : A.IsHermitian)
(i : n)
:
The diagonal elements of a complex Hermitian matrix are real.
theorem
Matrix.isHermitian_iff_isSymmetric
{α : Type u_1}
{n : Type u_4}
[RCLike α]
[Fintype n]
[DecidableEq n]
{A : Matrix n n α}
:
A matrix is Hermitian iff the corresponding linear map is self adjoint.