Almost Hermitian Matrices

This file contains the definition and some basic results about almost Hermitian matrices.

We say a matrix x is is_almost_hermitian if there exists some scalar α ∈ ℂ.

def Matrix.IsAlmostHermitian {𝕜 : Type u_1} {n : Type u_2} [Star 𝕜] [SMul 𝕜 (Matrix n n 𝕜)] (x : Matrix n n 𝕜) : Prop

a matrix $x \in M_n(\mathbb{k})$ is ``almost Hermitian'' if there exists some $\alpha\in\mathbb{k}$ and $y\in M_n(\mathbb{k})$ such that $\alpha y = x$ and $y$ is Hermitian

Equations

• x.IsAlmostHermitian = ∃ (α : 𝕜) (y : Matrix n n 𝕜), α • y = x ∧ y.IsHermitian

theorem Matrix.isAlmostHermitian_iff {n : Type u_1} (x : Matrix n n ℂ) : x.IsAlmostHermitian ↔ (kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) x x.conj).IsHermitian

$x\in M_n(\mathbb{C})$ is almost Hermitian if and only if $x \otimes_k \bar{x}$ is Hermitian

theorem Matrix.isAlmostHermitian_zero {𝕜 : Type u_1} {n : Type u_2} [Semiring 𝕜] [StarRing 𝕜] : IsAlmostHermitian 0

0 is almost Hermitian

theorem Matrix.AlmostHermitian.isStarNormal {𝕜 : Type u_2} {n : Type u_1} [Fintype n] [CommSemiring 𝕜] [StarRing 𝕜] {M : Matrix n n 𝕜} (hM : M.IsAlmostHermitian) : IsStarNormal M

if $x$ is almost Hermitian, then it is also normal

theorem Matrix.almost_hermitian_iff_smul {𝕜 : Type u_1} {n : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] {M : Matrix n n 𝕜} : M.IsAlmostHermitian ↔ ∀ (β : 𝕜), (β • M).IsAlmostHermitian

$x$ is almost Hermitian if and only if $\beta \cdot x$ is almost Hermitian for any $\beta$

def Matrix.IsDiagonal {R : Type u_1} {n : Type u_2} [Zero R] (A : Matrix n n R) : Prop

Equations

• A.IsDiagonal = ∀ (i j : n), i ≠ j → A i j = 0

theorem Matrix.isDiagonal_eq {n : Type u_2} {R : Type u_1} [Zero R] [DecidableEq n] (A : Matrix n n R) : A.IsDiagonal ↔ diagonal A.diag = A

theorem Matrix.IsAlmostHermitian.upper_triangular_iff_diagonal {𝕜 : Type u_1} {n : Type u_2} [Field 𝕜] [StarRing 𝕜] [LinearOrder n] {M : Matrix n n 𝕜} (hM : M.IsAlmostHermitian) : M.BlockTriangular id ↔ M.IsDiagonal

an almost Hermitian matrix is upper-triangular if and only if it is diagonal

theorem Matrix.IsHermitian.isAlmostHermitian {𝕜 : Type u_1} {n : Type u_2} [Semiring 𝕜] [Star 𝕜] {x : Matrix n n 𝕜} (hx : x.IsHermitian) : x.IsAlmostHermitian