Trace of a product of two diagonalizable operators via their eigenbasis overlaps

Let $E$ be a finite-dimensional complex inner-product space, and let $A,B:E\to E$ be complex-linear maps with $A$ symmetric (self-adjoint), i.e. $\langle Ax,y\rangle=\langle x,Ay\rangle$ for all $x,y\in E$. Let $(e_i)_{i\in\iota}$ and $(f_j)_{j\in\kappa}$ be orthonormal bases of $E$ indexed by finite sets $\iota,\kappa$, and let $a:\iota\to\mathbb R$, $b:\kappa\to\mathbb R$ be such that $e_i$ is an eigenvector of $A$ with eigenvalue $a_i$ ($A(e_i)=a_ie_i$) and $f_j$ is an eigenvector of $B$ with eigenvalue $b_j$ ($B(f_j)=b_jf_j$), for every $i,j$. Write the basis overlap $\operatorname{ov}(e_i,f_j)=|\langle e_i,f_j\rangle|^2$. Then

This expands the trace of a product of two diagonalizable operators, each given in its own eigenbasis, into a double sum over pairs of eigenvalues weighted by the squared overlaps of the two eigenbases. It is the key spectral-lift step: applied to the Hermitian dilations of two rectangular operators, it turns trace-level Bregman- and Mazur-type comparison quantities into sums, over pairs of eigenvalues, of the purely scalar Bregman/Mazur comparison — which is where dimension-independent constants can come from.

Formalization Note. Only $A$ is hypothesized symmetric; $B$ is given only through its eigen-relation $B(f_j)=b_jf_j$ with real $b$, not through a separate IsSymmetric hypothesis. This is not a genuinely broader class of operators than symmetric ones — an operator that is diagonal with real eigenvalues in some orthonormal basis is automatically self-adjoint — but the proof below never uses any self-adjointness fact about $B$, only the explicit eigen-data $(f,b)$, so stating the hypothesis this way records exactly what the argument needs, not a strictly weaker mathematical assumption. The same observation applies to $A$: the eigen-relation $A(e_i)=a_ie_i$ already forces $A$ to be self-adjoint, so the separately listed hypothesis that $A$ is symmetric is likewise implied by the eigen-data, not an independent restriction.