English
The continuous functional calculus for a Hermitian matrix can be realized as a triple product using the spectral decomposition: the matrix of a function f on the spectrum equals U diag(f(λ_i)) U*, with U the eigenvector unitary.
Русский
Непрерывный функциональный калькулятор эрмитовой матрицы реализуется как тройной продукт через спектральное разложение: матрица функции f на спектре равна U diag(f(λ_i)) U*, где U — единичная матрица собственных векторов.
LaTeX
$$$cfc(f) = (U) \; diag(f(λ_i)) \; (U)^*$, with $U = \text{eigenvectorUnitary}(A)$ and $λ_i$ eigenvalues$$
Lean4
/-- 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. -/
protected noncomputable def cfc (f : ℝ → ℝ) : Matrix n n 𝕜 :=
(eigenvectorUnitary hA : Matrix n n 𝕜) * diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues) *
star (eigenvectorUnitary hA : Matrix n n 𝕜)
