Matrix Spectra

Spectral helpers for Hermitian and almost-Hermitian matrices.

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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_3} (f : α → β) (s : Finset α) [CoeTC β γ] : Multiset.map (fun (x : β) => CoeTC.coe x) (Multiset.map f s.val) = Multiset.map (fun (x : α) => CoeTC.coe (f x)) s.val

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

@[implicit_reducible]

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

Equations

• multisetCoeTCRToRCLike = multisetCoeTC

@[implicit_reducible]

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

Equations

• multisetCoeRToRCLike = { coe := CoeTC.coe }

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

Choose a scalar and Hermitian matrix witnessing that an almost-Hermitian matrix is scalar Hermitian.

Equations

• One or more equations did not get rendered due to their size.

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

The scalar chosen from an almost-Hermitian witness.

Equations

• hx.scalar = hx.scalarMatrix.1

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

The Hermitian matrix chosen from an almost-Hermitian witness.

Equations

• hx.matrix = hx.scalarMatrix.2

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 → 𝕜

Eigenvalues of the Hermitian factor, rescaled by the almost-Hermitian scalar.

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 𝕜

Multiset of eigenvalues for an almost-Hermitian matrix.

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 ℝ

Multiset of real eigenvalues for a Hermitian matrix.

Equations

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

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)

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

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)

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

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 : ↥(unitaryGroup n 𝕜)) : ((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 : ↥(unitaryGroup n 𝕜)) : A.IsAlmostHermitian ↔ ((innerAut U) A).IsAlmostHermitian

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

A matrix has almost equal spectra to another if a nonzero scalar multiple has equal spectra.

Equations

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