@[protected, instance]
Equations
- multiset_coe = {coe := λ (s : multiset α), multiset.map coe s}
theorem
finset.val.map_coe
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(s : finset α)
[has_coe β γ] :
↑(multiset.map f s.val) = multiset.map ↑f s.val
@[protected, instance]
Equations
noncomputable
def
matrix.is_almost_hermitian.scalar
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
{n : Type u_1}
{x : matrix n n 𝕜}
(hx : x.is_almost_hermitian) :
𝕜
Equations
- hx.scalar = (λ (_x : ∃ (y : matrix n n 𝕜), classical.some hx • y = x ∧ y.is_hermitian), classical.some hx) _
noncomputable
def
matrix.is_almost_hermitian.matrix
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
{n : Type u_1}
{x : matrix n n 𝕜}
(hx : x.is_almost_hermitian) :
matrix n n 𝕜
Equations
- hx.matrix = (λ (_x : classical.some hx • classical.some _ = x ∧ (classical.some _).is_hermitian), classical.some _) _
theorem
matrix.is_almost_hermitian.eq_smul_matrix
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
{n : Type u_1}
{x : matrix n n 𝕜}
(hx : x.is_almost_hermitian) :
theorem
matrix.is_almost_hermitian.matrix_is_hermitian
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
{n : Type u_1}
{x : matrix n n 𝕜}
(hx : x.is_almost_hermitian) :
noncomputable
def
matrix.is_almost_hermitian.eigenvalues
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{x : matrix n n 𝕜}
(hx : x.is_almost_hermitian) :
n → 𝕜
Equations
- hx.eigenvalues = λ (i : n), hx.scalar • ↑(_.eigenvalues i)
noncomputable
def
matrix.is_almost_hermitian.spectra
{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) :
multiset 𝕜
Equations
- hA.spectra = multiset.map (λ (i : n), hA.eigenvalues i) finset.univ.val
noncomputable
def
matrix.is_hermitian.spectra
{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_hermitian) :
Equations
- hA.spectra = multiset.map (λ (i : n), hA.eigenvalues i) finset.univ.val
theorem
matrix.is_hermitian.spectra_coe
{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_hermitian) :
↑(hA.spectra) = multiset.map (λ (i : n), ↑(hA.eigenvalues i)) finset.univ.val
theorem
matrix.is_hermitian.mem_coe_spectra_diagonal
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{A : n → 𝕜}
(hA : (matrix.diagonal A).is_hermitian)
(x : 𝕜) :
theorem
matrix.is_hermitian.spectra_set_eq_spectrum
{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_hermitian) :
theorem
matrix.is_hermitian.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_hermitian)
(U : ↥(matrix.unitary_group n 𝕜)) :
(⇑(matrix.inner_aut U) A).is_hermitian
theorem
matrix.is_almost_hermitian_iff_smul
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{A : matrix n n 𝕜} :
A.is_almost_hermitian ↔ ∀ (α : 𝕜), (α • A).is_almost_hermitian
theorem
matrix.is_almost_hermitian.smul
{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)
(α : 𝕜) :
(α • A).is_almost_hermitian
theorem
matrix.is_almost_hermitian.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 𝕜)) :
(⇑(matrix.inner_aut U) A).is_almost_hermitian
theorem
matrix.is_almost_hermitian_iff_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 𝕜}
(U : ↥(matrix.unitary_group n 𝕜)) :
def
matrix.is_almost_hermitian.has_almost_equal_spectra_to
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{x y : matrix n n 𝕜}
(hx : x.is_almost_hermitian)
(hy : y.is_almost_hermitian) :
Prop
we say a matrix $x$ has almost equal spectra to another matrix $y$ if there exists some scalar $0\neq\beta \in \mathbb{C}$ such that $x$ and $\beta y$ have equal spectra