Real Spectral Functional Calculus Formula

Proved

FunctionalInequalities.Analysis.cfc_eq_mul_diagonal_mul_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This identifies the functional calculus of a finite real Hermitian matrix in an orthonormal eigenbasis.

Let $n$ be a finite index type, let $A\in M_n(\mathbb R)$ be Hermitian, and let $f:\mathbb R\to\mathbb R$ . If $U$ is the orthonormal eigenvector unitary of $A$ and $\lambda_i$ are its eigenvalues, then

\operatorname{cfc}(f,A)=U\,\operatorname{diag}(f(\lambda_i))\,U^{\mathsf T}.

The Lean declaration is cfc_eq_mul_diagonal_mul_readable. It is an exact finite-dimensional identity and does not assert any inequality or regularity property of $f$ .

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem cfc_eq_mul_diagonal_mul {A : Matrix n n ℝ} (hA : A.IsHermitian) (f : ℝ → ℝ) :
    cfc f A = (hA.eigenvectorUnitary : Matrix n n ℝ) * diagonal (fun i => f (hA.eigenvalues i)) *
      (hA.eigenvectorUnitary : Matrix n n ℝ)ᵀ

Module navigation

Module: Analysis/Matrix/Trace/Power.

Source excerpt, lines 170–172 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Trace_Power

open Matrix
variable {n : Type*} [Fintype n] [DecidableEq n]
variable {n : Type*} [Fintype n] [DecidableEq n]

Formal statement


theorem FunctionalInequalities.Analysis.cfc_eq_mul_diagonal_mul_readable {A : Matrix n n ℝ} (hA : A.IsHermitian) (f : ℝ → ℝ) :
    cfc f A = (hA.eigenvectorUnitary : Matrix n n ℝ) * diagonal (fun i => f (hA.eigenvalues i)) *
      (hA.eigenvectorUnitary : Matrix n n ℝ)ᵀ := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Matrix/Trace/Power.lean#L169-L194 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.Trace.Power`, declaration `FunctionalInequalities.Analysis.cfc_eq_mul_diagonal_mul`; the repository is private at upload time).

View graph