Documentation

Monlib.LinearAlgebra.Matrix.Spectra

instance multisetCoe {α : Type u_1} {β : Type u_2} [Coe α β] :
Equations
instance multisetCoeTC {α : Type u_1} {β : Type u_2} [CoeTC α β] :
Equations
theorem Finset.val.map_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (s : Finset α) [CoeTC β γ] :
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)
noncomputable instance multisetCoeTC_RToRCLike {𝕜 : Type u_1} [RCLike 𝕜] :
Equations
noncomputable instance multisetCoeRToRCLike {𝕜 : Type u_1} [RCLike 𝕜] :
Equations
noncomputable def Matrix.IsAlmostHermitian.scalar_matrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {x : Matrix n n 𝕜} (hx : x.IsAlmostHermitian) :
𝕜 × Matrix n n 𝕜
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    noncomputable def Matrix.IsAlmostHermitian.scalar {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {x : Matrix n n 𝕜} (hx : x.IsAlmostHermitian) :
    𝕜
    Equations
    Instances For
      noncomputable def Matrix.IsAlmostHermitian.matrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {x : Matrix n n 𝕜} (hx : x.IsAlmostHermitian) :
      Matrix n n 𝕜
      Equations
      Instances For
        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) :
        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
        Instances For
          noncomputable def Matrix.IsAlmostHermitian.spectra {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsAlmostHermitian) :
          Equations
          Instances For
            noncomputable def Matrix.IsHermitian.spectra {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :
            Equations
            Instances For
              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) :
              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 𝕜)) :
              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) (α : 𝕜) :
              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 𝕜)) :
              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 𝕜)) :
              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) :

              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
              Instances For