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

• Matrix.IsHermitian.cfc : Realization of the functional calculus for a Hermitian matrix as the triple product U * diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues) * star U with U = eigenvectorUnitary hA.

• cfc_eq : Proof that the above agrees with the continuous functional calculus.

• Matrix.IsHermitian.instContinuousFunctionalCalculus : Instance of the continuous functional calculus for a Hermitian matrix A over 𝕜.

Tags

spectral theorem, diagonalization theorem, continuous functional calculus

theorem Matrix.finite_real_spectrum {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} : (spectrum ℝ A).Finite

instance Matrix.instFiniteElemRealSpectrum {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} : Finite ↑(spectrum ℝ A)

Equations

• ⋯ = ⋯

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

@[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

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.

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

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

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

Equations

• ⋯ = ⋯

instance Matrix.IsHermitian.instUniqueContinuousFunctionalCalculus {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] : UniqueContinuousFunctionalCalculus ℝ (Matrix n n 𝕜)

Equations

• ⋯ = ⋯

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

• hA.cfc f = ↑hA.eigenvectorUnitary * Matrix.diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary

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