Hermitian matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines hermitian matrices and some basic results about them.
See also is_self_adjoint, which generalizes this definition to other star rings.
Main definition #
matrix.is_hermitian: 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.is_hermitian = (A.conj_transpose = A)
theorem
matrix.is_hermitian.eq
{α : Type u_1}
{n : Type u_4}
[has_star α]
{A : matrix n n α}
(h : A.is_hermitian) :
A.conj_transpose = A
@[protected]
theorem
matrix.is_hermitian.is_self_adjoint
{α : Type u_1}
{n : Type u_4}
[has_star α]
{A : matrix n n α}
(h : A.is_hermitian) :
@[ext]
theorem
matrix.is_hermitian.ext
{α : Type u_1}
{n : Type u_4}
[has_star α]
{A : matrix n n α} :
(∀ (i j : n), has_star.star (A j i) = A i j) → A.is_hermitian
theorem
matrix.is_hermitian.apply
{α : Type u_1}
{n : Type u_4}
[has_star α]
{A : matrix n n α}
(h : A.is_hermitian)
(i j : n) :
has_star.star (A j i) = A i j
theorem
matrix.is_hermitian.ext_iff
{α : Type u_1}
{n : Type u_4}
[has_star α]
{A : matrix n n α} :
A.is_hermitian ↔ ∀ (i j : n), has_star.star (A j i) = A i j
@[simp]
theorem
matrix.is_hermitian.map
{α : Type u_1}
{β : Type u_2}
{n : Type u_4}
[has_star α]
[has_star β]
{A : matrix n n α}
(h : A.is_hermitian)
(f : α → β)
(hf : function.semiconj f has_star.star has_star.star) :
(A.map f).is_hermitian
theorem
matrix.is_hermitian.transpose
{α : Type u_1}
{n : Type u_4}
[has_star α]
{A : matrix n n α}
(h : A.is_hermitian) :
@[simp]
theorem
matrix.is_hermitian_transpose_iff
{α : Type u_1}
{n : Type u_4}
[has_star α]
(A : matrix n n α) :
theorem
matrix.is_hermitian.conj_transpose
{α : Type u_1}
{n : Type u_4}
[has_star α]
{A : matrix n n α}
(h : A.is_hermitian) :
@[simp]
theorem
matrix.is_hermitian.submatrix
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[has_star α]
{A : matrix n n α}
(h : A.is_hermitian)
(f : m → n) :
(A.submatrix f f).is_hermitian
@[simp]
theorem
matrix.is_hermitian_submatrix_equiv
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[has_star α]
{A : matrix n n α}
(e : m ≃ n) :
(A.submatrix ⇑e ⇑e).is_hermitian ↔ A.is_hermitian
@[simp]
theorem
matrix.is_hermitian_conj_transpose_iff
{α : Type u_1}
{n : Type u_4}
[has_involutive_star α]
(A : matrix n n α) :
theorem
matrix.is_hermitian.from_blocks
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[has_involutive_star α]
{A : matrix m m α}
{B : matrix m n α}
{C : matrix n m α}
{D : matrix n n α}
(hA : A.is_hermitian)
(hBC : B.conj_transpose = C)
(hD : D.is_hermitian) :
(matrix.from_blocks A B C D).is_hermitian
A block matrix A.from_blocks B C D is hermitian,
if A and D are hermitian and Bᴴ = C.
theorem
matrix.is_hermitian_from_blocks_iff
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[has_involutive_star α]
{A : matrix m m α}
{B : matrix m n α}
{C : matrix n m α}
{D : matrix n n α} :
(matrix.from_blocks A B C D).is_hermitian ↔ A.is_hermitian ∧ B.conj_transpose = C ∧ C.conj_transpose = B ∧ D.is_hermitian
This is the iff version of matrix.is_hermitian.from_blocks.
theorem
matrix.is_hermitian_diagonal_of_self_adjoint
{α : Type u_1}
{n : Type u_4}
[add_monoid α]
[star_add_monoid α]
[decidable_eq n]
(v : n → α)
(h : is_self_adjoint v) :
A diagonal matrix is hermitian if the entries are self-adjoint
@[simp]
theorem
matrix.is_hermitian_diagonal
{α : Type u_1}
{n : Type u_4}
[add_monoid α]
[star_add_monoid α]
[has_trivial_star α]
[decidable_eq 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.is_hermitian.add
{α : Type u_1}
{n : Type u_4}
[add_monoid α]
[star_add_monoid α]
{A B : matrix n n α}
(hA : A.is_hermitian)
(hB : B.is_hermitian) :
(A + B).is_hermitian
theorem
matrix.is_hermitian_add_transpose_self
{α : Type u_1}
{n : Type u_4}
[add_comm_monoid α]
[star_add_monoid α]
(A : matrix n n α) :
(A + A.conj_transpose).is_hermitian
theorem
matrix.is_hermitian_transpose_add_self
{α : Type u_1}
{n : Type u_4}
[add_comm_monoid α]
[star_add_monoid α]
(A : matrix n n α) :
(A.conj_transpose + A).is_hermitian
@[simp]
theorem
matrix.is_hermitian.neg
{α : Type u_1}
{n : Type u_4}
[add_group α]
[star_add_monoid α]
{A : matrix n n α}
(h : A.is_hermitian) :
(-A).is_hermitian
@[simp]
theorem
matrix.is_hermitian.sub
{α : Type u_1}
{n : Type u_4}
[add_group α]
[star_add_monoid α]
{A B : matrix n n α}
(hA : A.is_hermitian)
(hB : B.is_hermitian) :
(A - B).is_hermitian
theorem
matrix.is_hermitian_mul_conj_transpose_self
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[non_unital_semiring α]
[star_ring α]
[fintype n]
(A : matrix m n α) :
(A.mul A.conj_transpose).is_hermitian
Note this is more general than is_self_adjoint.mul_star_self as B can be rectangular.
theorem
matrix.is_hermitian_transpose_mul_self
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[non_unital_semiring α]
[star_ring α]
[fintype m]
(A : matrix m n α) :
(A.conj_transpose.mul A).is_hermitian
Note this is more general than is_self_adjoint.star_mul_self as B can be rectangular.
theorem
matrix.is_hermitian_conj_transpose_mul_mul
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[non_unital_semiring α]
[star_ring α]
[fintype m]
{A : matrix m m α}
(B : matrix m n α)
(hA : A.is_hermitian) :
((B.conj_transpose.mul A).mul B).is_hermitian
Note this is more general than is_self_adjoint.conjugate' as B can be rectangular.
theorem
matrix.is_hermitian_mul_mul_conj_transpose
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
[non_unital_semiring α]
[star_ring α]
[fintype m]
{A : matrix m m α}
(B : matrix n m α)
(hA : A.is_hermitian) :
((B.mul A).mul B.conj_transpose).is_hermitian
Note this is more general than is_self_adjoint.conjugate as B can be rectangular.
@[simp]
theorem
matrix.is_hermitian_one
{α : Type u_1}
{n : Type u_4}
[semiring α]
[star_ring α]
[decidable_eq n] :
Note this is more general for matrices than is_self_adjoint_one as it does not
require fintype n, which is necessary for monoid (matrix n n R).
theorem
matrix.is_hermitian.inv
{α : Type u_1}
{m : Type u_3}
[comm_ring α]
[star_ring α]
[fintype m]
[decidable_eq m]
{A : matrix m m α}
(hA : A.is_hermitian) :
@[simp]
theorem
matrix.is_hermitian_inv
{α : Type u_1}
{m : Type u_3}
[comm_ring α]
[star_ring α]
[fintype m]
[decidable_eq m]
(A : matrix m m α)
[invertible A] :
theorem
matrix.is_hermitian.adjugate
{α : Type u_1}
{m : Type u_3}
[comm_ring α]
[star_ring α]
[fintype m]
[decidable_eq m]
{A : matrix m m α}
(hA : A.is_hermitian) :
theorem
matrix.is_hermitian.coe_re_apply_self
{α : Type u_1}
{n : Type u_4}
[is_R_or_C α]
{A : matrix n n α}
(h : A.is_hermitian)
(i : n) :
↑(⇑is_R_or_C.re (A i i)) = A i i
The diagonal elements of a complex hermitian matrix are real.
theorem
matrix.is_hermitian.coe_re_diag
{α : Type u_1}
{n : Type u_4}
[is_R_or_C α]
{A : matrix n n α}
(h : A.is_hermitian) :
The diagonal elements of a complex hermitian matrix are real.
theorem
matrix.is_hermitian_iff_is_symmetric
{α : Type u_1}
{n : Type u_4}
[is_R_or_C α]
[fintype n]
[decidable_eq n]
{A : matrix n n α} :
A matrix is hermitian iff the corresponding linear map is self adjoint.