Hermitian form of a spectral function in eigenbasis coordinates: $\operatorname{Re}(x^{\mathsf H} f(A) x) = \sum_i f(\lambda_i)\|c_i\|^2$

Let $A$ be an $n \times n$ Hermitian matrix over an RCLike field $\mathbb{K}$, with spectral decomposition $A = U \operatorname{diag}(\lambda) U^{\mathsf H}$ ($U$ the eigenvector unitary, $\lambda_i$ the eigenvalues). For a real function $f : \mathbb{R} \to \mathbb{R}$, the project defines the spectral functional calculus

Statement. For every vector $x \in \mathbb{K}^n$, writing $c = U^{\mathsf H} x$ for its eigenbasis coordinates,

That is, the Hermitian quadratic form of $f(A)$ diagonalizes in the eigenbasis of $A$ with weights $f(\lambda_i)$. In the module Zeta23.LinAlg.HermitianPosPart this identity drives the positivity statements about the Hermitian positive part $A_+ = \operatorname{specMap}(A, t \mapsto t^+)$: it is consumed by RHLinalg.posDefOn_range_hermPosPart (Sylvester, easy direction) and by Zeta23.Tail.traceNorm_le_of_hasSum_vecMulVec in the tail estimates of the matrix-variational argument.