Documentation

Mathlib.LinearAlgebra.Matrix.Hermitian

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 #

Tags #

self-adjoint matrix, hermitian matrix

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
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) :
    star (A j i) = A i j
    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) :
    @[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 : mn) :
    @[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) :
    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) :

    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 α} :

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

    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α) :

    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) :
    @[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) :

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

    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) :

    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) :

    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) :
    @[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 : ) :
    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.zpow {α : Type u_1} {m : Type u_3} [CommRing α] [StarRing α] [Fintype m] [DecidableEq m] {A : Matrix m m α} (h : 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.