Monlib.LinearAlgebra.Matrix.Spectra

source

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

Coe (Multiset α) (Multiset β)

Equations

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

source

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

CoeTC (Multiset α) (Multiset β)

Equations

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

source

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

Multiset.map CoeTC.coe (Multiset.map f s.val) = Multiset.map CoeTC.coe (Multiset.map f s.val)

source

theorem Finset.val.map_coe' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (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)

source

noncomputable instance multisetCoeTC_RToRCLike {𝕜 : Type u_1} [RCLike 𝕜] :

CoeTC (Multiset ℝ) (Multiset 𝕜)

Equations

multisetCoeTC_RToRCLike = multisetCoeTC

source

noncomputable instance multisetCoeRToRCLike {𝕜 : Type u_1} [RCLike 𝕜] :

Coe (Multiset ℝ) (Multiset 𝕜)

Equations

multisetCoeRToRCLike = { coe := CoeTC.coe }

source

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) ⋯

Instances For

source

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 ⋯) ⋯

Instances For

source

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

source

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

hx.matrix.IsHermitian

source

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)

Instances For

source

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

Instances For

source

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

Instances For

source

theorem Matrix.IsHermitian.spectra_coe {n : Type u_1} {𝕜 : Type u_2} [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)

source

theorem Matrix.IsHermitian.mem_coe_spectra_diagonal {n : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : n → 𝕜} (hA : (diagonal A).IsHermitian) (x : 𝕜) :

x ∈ Multiset.map RCLike.ofReal hA.spectra ↔ ∃ (i : n), A i = x

source

theorem Matrix.IsHermitian.spectra_set_eq_spectrum {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :

{x : 𝕜 | x ∈ Multiset.map RCLike.ofReal hA.spectra} = _root_.spectrum 𝕜 (toLin' A)

source

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 : ↥(unitaryGroup n 𝕜)) :

((innerAut U) A).IsHermitian

source

theorem Matrix.isAlmostHermitian_iff_smul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {A : Matrix n n 𝕜} :

A.IsAlmostHermitian ↔ ∀ (α : 𝕜), (α • A).IsAlmostHermitian

source

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

(α • A).IsAlmostHermitian

source

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 : ↥(unitaryGroup n 𝕜)) :

((innerAut U) A).IsAlmostHermitian

source

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

A.IsAlmostHermitian ↔ ((innerAut U) A).IsAlmostHermitian

source

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

Instances For