instance multisetCoe {α : Type u_1} {β : Type u_2} [Coe α β] : Coe (Multiset α) (Multiset β)

Equations

• multisetCoe = { coe := fun (s : Multiset α) => Multiset.map Coe.coe s }

instance multisetCoeTC {α : Type u_1} {β : Type u_2} [CoeTC α β] : CoeTC (Multiset α) (Multiset β)

Equations

• multisetCoeTC = { coe := fun (s : Multiset α) => Multiset.map CoeTC.coe s }

theorem Finset.val.map_coe {α : Type u_1} {β : Type u_2} {γ : Type u_2} (f : α → β) (s : Finset α) [CoeTC β γ] : Multiset.map CoeTC.coe (Multiset.map f s.val) = Multiset.map CoeTC.coe (Multiset.map f s.val)

theorem Finset.val.map_coe' {α : Type u_1} {β : Type u_2} {γ : Type u_2} (f : α → β) (s : Finset α) [Coe β γ] : Multiset.map (fun (a : β) => Coe.coe a) (Multiset.map f s.val) = Multiset.map (fun (a : β) => Coe.coe a) (Multiset.map f s.val)

noncomputable instance multisetCoeTC_RToRCLike {𝕜 : Type u_1} [RCLike 𝕜] : CoeTC (Multiset ℝ) (Multiset 𝕜)

Equations

• multisetCoeTC_RToRCLike = multisetCoeTC

noncomputable instance multisetCoeRToRCLike {𝕜 : Type u_1} [RCLike 𝕜] : Coe (Multiset ℝ) (Multiset 𝕜)

Equations

• multisetCoeRToRCLike = { coe := CoeTC.coe }

noncomputable def Matrix.IsAlmostHermitian.scalar {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {x : Matrix n n 𝕜} (hx : x.IsAlmostHermitian) : 𝕜

Equations

• hx.scalar = (fun (α : 𝕜) (x : ∃ (y : Matrix n n 𝕜), α • y = x ∧ y.IsHermitian) => α) (Classical.choose hx) ⋯

noncomputable def Matrix.IsAlmostHermitian.matrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {x : Matrix n n 𝕜} (hx : x.IsAlmostHermitian) : Matrix n n 𝕜

Equations

• hx.matrix = (fun (y : Matrix n n 𝕜) (x : Classical.choose hx • y = x ∧ y.IsHermitian) => y) (Classical.choose ⋯) ⋯

theorem Matrix.IsAlmostHermitian.eq_smul_matrix {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} {x : Matrix n n 𝕜} (hx : x.IsAlmostHermitian) : x = hx.scalar • hx.matrix

theorem Matrix.IsAlmostHermitian.matrix_isHermitian {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} {x : Matrix n n 𝕜} (hx : x.IsAlmostHermitian) : hx.matrix.IsHermitian

noncomputable def Matrix.IsAlmostHermitian.eigenvalues {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.IsAlmostHermitian) : n → 𝕜

Equations

• hx.eigenvalues i = hx.scalar • ↑(⋯.eigenvalues i)

noncomputable def Matrix.IsAlmostHermitian.spectra {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsAlmostHermitian) : Multiset 𝕜

Equations

• hA.spectra = Multiset.map (fun (i : n) => hA.eigenvalues i) Finset.univ.val

noncomputable def Matrix.IsHermitian.spectra {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : Multiset ℝ

Equations

• hA.spectra = Multiset.map (fun (i : n) => hA.eigenvalues i) Finset.univ.val

theorem Matrix.IsHermitian.spectra_coe {n : Type u_1} {𝕜 : Type} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : Multiset.map RCLike.ofReal hA.spectra = Multiset.map RCLike.ofReal (Multiset.map (fun (i : n) => hA.eigenvalues i) Finset.univ.val)

theorem Matrix.IsHermitian.mem_coe_spectra_diagonal {n : Type u_1} {𝕜 : Type} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : n → 𝕜} (hA : (Matrix.diagonal A).IsHermitian) (x : 𝕜) : x ∈ Multiset.map RCLike.ofReal hA.spectra ↔ ∃ (i : n), A i = x

theorem Matrix.IsHermitian.spectra_set_eq_spectrum {n : Type u_1} {𝕜 : Type} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : {x : 𝕜 | x ∈ Multiset.map RCLike.ofReal hA.spectra} = spectrum 𝕜 (Matrix.toLin' A)

theorem Matrix.IsHermitian.of_innerAut {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (U : ↥(Matrix.unitaryGroup n 𝕜)) : ((Matrix.innerAut U) A).IsHermitian

theorem Matrix.isAlmostHermitian_iff_smul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} : A.IsAlmostHermitian ↔ ∀ (α : 𝕜), (α • A).IsAlmostHermitian

theorem Matrix.IsAlmostHermitian.smul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsAlmostHermitian) (α : 𝕜) : (α • A).IsAlmostHermitian

theorem Matrix.IsAlmostHermitian.of_innerAut {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsAlmostHermitian) (U : ↥(Matrix.unitaryGroup n 𝕜)) : ((Matrix.innerAut U) A).IsAlmostHermitian

theorem Matrix.isAlmostHermitian_iff_of_innerAut {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (U : ↥(Matrix.unitaryGroup n 𝕜)) : A.IsAlmostHermitian ↔ ((Matrix.innerAut U) A).IsAlmostHermitian

def Matrix.IsAlmostHermitian.HasAlmostEqualSpectraTo {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} {y : Matrix n n 𝕜} (hx : x.IsAlmostHermitian) (hy : y.IsAlmostHermitian) : 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

Equations

• hx.HasAlmostEqualSpectraTo hy = ∃ (β : 𝕜ˣ), hx.spectra = ⋯.spectra