Documentation

Monlib.LinearAlgebra.Matrix.IsAlmostHermitian

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 α ∈ ℂ.

source
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
Instances For
    source
    theorem Matrix.isAlmostHermitian_iff {n : Type u_1} (x : Matrix n n ℂ) :
    x.IsAlmostHermitian ↔ (Matrix.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

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

    0 is almost Hermitian

    source
    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

    source
    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$

    source
    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
    Instances For
      source
      theorem Matrix.isDiagonal_eq {n : Type u_2} {R : Type u_1} [Zero R] [DecidableEq n] (A : Matrix n n R) :
      A.IsDiagonal ↔ Matrix.diagonal A.diag = A
      source
      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

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