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

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.

@[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 = ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ ⇑g ∘ fun (i : n) => ⟨hA.eigenvalues i, ⋯⟩))

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

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 ℝ (Matrix n n 𝕜) IsSelfAdjoint

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

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 = ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (Matrix.diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues))

theorem Matrix.IsHermitian.cfcHom_eq_cfcAux {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : cfcHom ⋯ = hA.cfcAux

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

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

theorem Matrix.IsHermitian.charpoly_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).charpoly = ∏ i : n, (Polynomial.X - Polynomial.C ↑(f (hA.eigenvalues i)))