mathlib documentation

linear_algebra.matrix.hermitian

Hermitian matrices #

This file defines hermitian matrices and some basic results about them.

Main definition #

Tags #

self-adjoint matrix, hermitian matrix

def matrix.is_hermitian {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] (A : matrix n n α) :
Prop

A matrix is hermitian if it is equal to its conjugate transpose. On the reals, this definition captures symmetric matrices.

Equations
theorem matrix.is_hermitian.eq {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] {A : matrix n n α} (h : A.is_hermitian) :
@[ext]
theorem matrix.is_hermitian.ext {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] {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} [non_unital_semiring α] [star_ring α] {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} [non_unital_semiring α] [star_ring α] {A : matrix n n α} :
A.is_hermitian ∀ (i j : n), has_star.star (A j i) = A i j
theorem matrix.is_hermitian_mul_conj_transpose_self {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] [fintype n] (A : matrix n n α) :
theorem matrix.is_hermitian_transpose_mul_self {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] [fintype n] (A : matrix n n α) :
theorem matrix.is_hermitian_add_transpose_self {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] (A : matrix n n α) :
theorem matrix.is_hermitian_transpose_add_self {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] (A : matrix n n α) :
@[simp]
theorem matrix.is_hermitian_zero {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] :
@[simp]
theorem matrix.is_hermitian.map {α : Type u_1} {β : Type u_2} {n : Type u_4} [non_unital_semiring α] [star_ring α] [non_unital_semiring β] [star_ring β] {A : matrix n n α} (h : A.is_hermitian) (f : α → β) (hf : function.semiconj f has_star.star has_star.star) :
@[simp]
theorem matrix.is_hermitian.transpose {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] {A : matrix n n α} (h : A.is_hermitian) :
@[simp]
theorem matrix.is_hermitian.conj_transpose {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] {A : matrix n n α} (h : A.is_hermitian) :
@[simp]
theorem matrix.is_hermitian.add {α : Type u_1} {n : Type u_4} [non_unital_semiring α] [star_ring α] {A B : matrix n n α} (hA : A.is_hermitian) (hB : B.is_hermitian) :
@[simp]
theorem matrix.is_hermitian.minor {α : Type u_1} {m : Type u_3} {n : Type u_4} [non_unital_semiring α] [star_ring α] {A : matrix n n α} (h : A.is_hermitian) (f : m → n) :
@[simp]
theorem matrix.is_hermitian_diagonal {n : Type u_4} [decidable_eq n] (v : n → ) :

The real diagonal matrix diagonal v is hermitian.

theorem matrix.is_hermitian.from_blocks {α : Type u_1} {m : Type u_3} {n : Type u_4} [non_unital_semiring α] [star_ring α] {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) :

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} [non_unital_semiring α] [star_ring α] {A : matrix m m α} {B : matrix m n α} {C : matrix n m α} {D : matrix n n α} :

This is the iff version of matrix.is_hermitian.from_blocks.

@[simp]
theorem matrix.is_hermitian_one {α : Type u_1} {n : Type u_4} [semiring α] [star_ring α] [decidable_eq n] :
@[simp]
theorem matrix.is_hermitian.neg {α : Type u_1} {n : Type u_4} [ring α] [star_ring α] {A : matrix n n α} (h : A.is_hermitian) :
@[simp]
theorem matrix.is_hermitian.sub {α : Type u_1} {n : Type u_4} [ring α] [star_ring α] {A B : matrix n n α} (hA : A.is_hermitian) (hB : B.is_hermitian) :
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.