The spectral Bregman trace as an overlap-weighted sum of scalar Bregman terms

Fix a finite-dimensional complex inner-product space $E$ and a real number $p$ (no hypothesis is placed on $p$). Let $(e_i)_{i\in\iota}$ and $(f_j)_{j\in\kappa}$ be orthonormal bases of $E$ indexed by finite index types $\iota,\kappa$, and let $a:\iota\to\mathbb R$, $b:\kappa\to\mathbb R$ be real numbers attached to them. For an orthonormal basis $e$ and real numbers $c$, write $\mathrm{diag}_e(c)$ for the self-adjoint operator on $E$ with $\mathrm{diag}_e(c)\,e_i = c_i\,e_i$ for every $i$ (spectralDiagonal), and for a function $h:\mathbb R\to\mathbb R$ write $h(c)$ for the tuple $i\mapsto h(c_i)$, so $\mathrm{diag}_e(h(c))$ is the operator with eigenvalues $h(c_i)$; we also write $h(\mathrm{diag}_e(c))$ for this same operator.

With $F_p(x) = |x|^p/p$ and $G_p(x) = |x|^{p-2}x$, the spectral Bregman trace of $(e,a)$ against $(f,b)$ is

(spectralBregmanTrace). The first, second and fourth traces are traces of operators diagonal with real entries. The cross term is the real trace of a product of two self-adjoint operators; its reality also follows from $\overline{\operatorname{Tr}(AB)}=\operatorname{Tr}(BA)=\operatorname{Tr}(AB)$. The product itself need not be self-adjoint. Write $\operatorname{ov}(e_i,f_j) = |\langle e_i,f_j\rangle|^2$ for the squared overlap of two basis vectors (orthonormalBasisOverlap), and

for the scalar Bregman quantity of $F_p$ (scalarBregman). The theorem states

This is one of two exact finite double-sum decompositions (the other is for the squared spectral Mazur distance) that let a scalar comparison between $\beta_p(x,y)$ and a Mazur-type quantity, once it is known to hold for every pair of real numbers, be summed against the overlap weights $\operatorname{ov}(e_i,f_j)$ — which are nonnegative and sum to $1$ along every row and column — and so lift unchanged, with the same constants, to a comparison between traces of finite-dimensional Hermitian operators.

Formalization Note The identity holds for every real $p$, including $p\le0$ or $p\in(0,1)$, because $F_p$, $G_p$, and division are all totalized in Lean: $F_p(0)=|0|^p/p$ evaluates to $0$ for every real $p$ (for $p\ne0$ because $0^p=0$; for $p=0$ because $0^0=1$ but $1/0=0$). This theorem asserts an algebraic trace identity, with no nonnegativity conclusion. For $p>1$, $F_p$ is convex and differentiable everywhere with derivative $G_p$, giving the usual Bregman-divergence interpretation used later in the argument.