Documentation

Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus

Continuous Functional Calculus for Hermitian Matrices #

This file defines an instance of the continuous functional calculus for Hermitian matrices over an RCLike field 𝕜.

Main Results #

Tags #

spectral theorem, diagonalization theorem, continuous functional calculus

source
theorem Matrix.finite_real_spectrum {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} :
(spectrum ℝ A).Finite
source
instance Matrix.instFiniteElemRealSpectrum {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} :
Finite ↑(spectrum ℝ A)
source
theorem Matrix.IsHermitian.eigenvalues_eq_spectrum_real {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {a : Matrix n n 𝕜} (ha : a.IsHermitian) :
spectrum ℝ a = Set.range ha.eigenvalues

The ℝ-spectrum of a Hermitian matrix over RCLike field is the range of the eigenvalue function

source
noncomputable def Matrix.IsHermitian.cfcAux {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :
C(↑(spectrum ℝ A), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜

The star algebra homomorphism underlying the instance of the continuous functional calculus of a Hermitian matrix. This is an auxiliary definition and is not intended for use outside of this file.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Matrix.IsHermitian.cfcAux_apply {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (g : C(↑(spectrum ℝ A), ℝ)) :
    hA.cfcAux g = ↑hA.eigenvectorUnitary * Matrix.diagonal (RCLike.ofReal ∘ ⇑g ∘ fun (i : n) => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary
    source
    theorem Matrix.IsHermitian.isClosedEmbedding_cfcAux {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :
    Topology.IsClosedEmbedding ⇑hA.cfcAux
    source
    @[deprecated Matrix.IsHermitian.isClosedEmbedding_cfcAux]
    theorem Matrix.IsHermitian.closedEmbedding_cfcAux {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :
    Topology.IsClosedEmbedding ⇑hA.cfcAux

    Alias of Matrix.IsHermitian.isClosedEmbedding_cfcAux.

    source
    theorem Matrix.IsHermitian.cfcAux_id {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :
    hA.cfcAux (ContinuousMap.restrict (spectrum ℝ A) (ContinuousMap.id ℝ)) = A
    source
    instance Matrix.IsHermitian.instContinuousFunctionalCalculus {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] :
    ContinuousFunctionalCalculus ℝ IsSelfAdjoint

    Instance of the continuous functional calculus for a Hermitian matrix over 𝕜 with RCLike 𝕜.

    source
    instance Matrix.IsHermitian.instUniqueContinuousFunctionalCalculus {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] :
    UniqueContinuousFunctionalCalculus ℝ (Matrix n n 𝕜)
    source
    noncomputable def Matrix.IsHermitian.cfc {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (f : ℝ → ℝ) :
    Matrix n n 𝕜

    The continuous functional calculus of a Hermitian matrix as a triple product using the spectral theorem. Note that this actually operates on bare functions since every function is continuous on the spectrum of a matrix, since the spectrum is finite. This is shown to be equal to the generic continuous functional calculus API in Matrix.IsHermitian.cfc_eq. In general, users should prefer the generic API, especially because it will make rewriting easier.

    Equations
    Instances For
      source
      theorem Matrix.IsHermitian.cfc_eq {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (f : ℝ → ℝ) :
      cfc f A = hA.cfc f