Rank of a spectral function of a Hermitian matrix: $\operatorname{rank} f(A) = \#\{i : f(\lambda_i) \ne 0\}$

Let $A$ be an $n \times n$ Hermitian matrix over an RCLike field with eigenvalues $\lambda_1, \dots, \lambda_n$, and for $f : \mathbb{R} \to \mathbb{R}$ let $\operatorname{specMap}(A, f) = U \operatorname{diag}(f(\lambda_i)) U^{\mathsf H}$ be the spectral functional calculus applied to $A$.

Statement.

the number of indices at which $f$ does not annihilate the corresponding eigenvalue.

Since conjugation by the unitary $U$ preserves rank, this reduces to the rank of a diagonal matrix. In the module Zeta23.LinAlg.HermitianPosPart this bookkeeping identity is used pervasively across the linear-algebra layer: it feeds RHLinalg.finrank_le_posIndex_of_posDefOn, RHLinalg.posIndex_add_le, RHLinalg.rank_trace_ineq, and the zero-side estimates Zeta23.ZeroSide.ZeroBlockData.posIndex_blockA_le, posIndex_blockQ_le, and Zeta23.ZeroSide.posIndex_smul_pos — in particular identifying the rank of the positive part $A_+$ with the positive index $n_+(A)$.