# 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

The `ℝ`

-spectrum of a Hermitian matrix over `RCLike`

field is the range of the eigenvalue
function

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

Instance of the continuous functional calculus for a Hermitian matrix over `𝕜`

with
`RCLike 𝕜`

.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

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.