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.is_almost_hermitian
{𝕜 : Type u_1}
{n : Type u_2}
[has_star 𝕜]
[has_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.is_almost_hermitian = ∃ (α : 𝕜) (y : matrix n n 𝕜), α • y = x ∧ y.is_hermitian
$x\in M_n(\mathbb{C})$ is almost Hermitian if and only if $x \otimes_k \bar{x}$ is Hermitian
0 is almost Hermitian
theorem
matrix.almost_hermitian.is_star_normal
{𝕜 : Type u_1}
{n : Type u_2}
[fintype n]
[comm_semiring 𝕜]
[star_ring 𝕜]
{M : matrix n n 𝕜}
(hM : M.is_almost_hermitian) :
if $x$ is almost Hermitian, then it is also normal
theorem
matrix.almost_hermitian_iff_smul
{𝕜 : Type u_1}
{n : Type u_2}
[comm_semiring 𝕜]
[star_ring 𝕜]
{M : matrix n n 𝕜} :
M.is_almost_hermitian ↔ ∀ (β : 𝕜), (β • M).is_almost_hermitian
$x$ is almost Hermitian if and only if $\beta \cdot x$ is almost Hermitian for any $\beta$
theorem
matrix.is_diagonal_eq
{n : Type u_2}
{R : Type u_1}
[has_zero R]
[decidable_eq n]
(A : matrix n n R) :
A.is_diagonal ↔ matrix.diagonal A.diag = A
theorem
matrix.is_almost_hermitian.upper_triangular_iff_diagonal
{𝕜 : Type u_1}
{n : Type u_2}
[field 𝕜]
[star_ring 𝕜]
[linear_order n]
{M : matrix n n 𝕜}
(hM : M.is_almost_hermitian) :
an almost Hermitian matrix is upper-triangular if and only if it is diagonal
theorem
matrix.is_hermitian.is_almost_hermitian
{𝕜 : Type u_1}
{n : Type u_2}
[semiring 𝕜]
[has_star 𝕜]
{x : matrix n n 𝕜}
(hx : x.is_hermitian) :