Some stuff on almost-Hermitian matrices #

This file contains a blackbox theorem that says that two almost-Hermitian matrices have the same spectrum if and only if they are almost similar. This is a generalization of the fact that two Hermitian matrices have the same spectrum if and only if they are unitarily similar.

source

theorem ite_eq_ite_iff {α : Type u_1} (a b c : α) :

(∀ {p : Prop} [_inst_1 : decidable p], ite p a c = ite p b c) ↔ a = b

source

theorem ite_eq_ite_iff_of_pi {n : Type u_1} {α : Type u_2} [decidable_eq n] (a b c : n → α) :

(∀ (i j : n), ite (i = j) (a i) (c i) = ite (i = j) (b i) (c i)) ↔ a = b

source

theorem matrix.is_almost_hermitian.spectra_ext {n : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] [decidable_eq 𝕜] {A B : n → 𝕜} (hA : (matrix.diagonal A).is_almost_hermitian) (hB : (matrix.diagonal B).is_almost_hermitian) :

hA.spectra = hB.spectra ↔ ∃ (σ : equiv.perm n), ∀ (i : n), A i = B (⇑σ i)

Note: this declaration is incomplete and uses sorry.

source

theorem matrix.is_diagonal.spectrum_eq_iff_rotation {n : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] [decidable_eq 𝕜] (A₁ A₂ : n → 𝕜) (hA₁ : (matrix.diagonal A₁).is_almost_hermitian) (hA₂ : (matrix.diagonal A₂).is_almost_hermitian) :

hA₁.spectra = hA₂.spectra ↔ ∃ (U : equiv.perm n), matrix.diagonal A₂ = ⇑(matrix.inner_aut ⟨(equiv.to_pequiv U).to_matrix, _⟩⁻¹) (matrix.diagonal A₁)

source

theorem matrix.is_almost_hermitian.spectra_of_inner_aut {n : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] [decidable_eq 𝕜] {A : matrix n n 𝕜} (hA : A.is_almost_hermitian) (U : ↥(matrix.unitary_group n 𝕜)) :

_.spectra = hA.spectra

Note: this declaration is incomplete and uses sorry.

source

theorem matrix.is_almost_hermitian.inner_aut_spectra {n : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] [decidable_eq 𝕜] {A : matrix n n 𝕜} (U : ↥(matrix.unitary_group n 𝕜)) (hA : (⇑(matrix.inner_aut U) A).is_almost_hermitian) :

hA.spectra = _.spectra

source

theorem matrix.is_almost_hermitian.spectrum_eq_iff {n : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] [decidable_eq 𝕜] {A₁ A₂ : matrix n n 𝕜} (hA₁ : A₁.is_almost_hermitian) (hA₂ : A₂.is_almost_hermitian) :

hA₁.spectra = hA₂.spectra ↔ ∃ (U : ↥(matrix.unitary_group n 𝕜)), A₂ = ⇑(matrix.inner_aut U⁻¹) A₁

source

def matrix.is_almost_similar_to {n : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] [fintype n] [decidable_eq n] [is_R_or_C 𝕜] (x y : matrix n n 𝕜) :

Prop

two matrices are almost similar if there exists some $0\neq\beta\in\mathbb{C}$ such that $x$ and $\beta y$ are similar

Equations

x.is_almost_similar_to y = ∃ (β : 𝕜ˣ) (U : ↥(matrix.unitary_group n 𝕜)), ↑β • y = ⇑(matrix.inner_aut U⁻¹) x

source

theorem matrix.is_almost_hermitian.has_almost_equal_spectra_to_iff_is_almost_similar_to {n : Type u_1} [fintype n] [decidable_eq n] [linear_order n] {x y : matrix n n ℂ} (hx : x.is_almost_hermitian) (hy : y.is_almost_hermitian) :

hx.has_almost_equal_spectra_to hy ↔ x.is_almost_similar_to y

an immediate corollary to matrix.is_almost_hermitian.spectrum_eq_iff using matrix.is_almost_similar_to and matrix.has_almost_equal_spectra_to