$\operatorname{Re}\operatorname{tr}(AB)$ as an eigenvalue bilinear form through $\|W_{kl}\|^2$

Let $A, B$ be $n \times n$ Hermitian matrices over an RCLike field, with spectral decompositions $A = U_A \operatorname{diag}(\lambda(A)) U_A^{\mathsf H}$ and $B = U_B \operatorname{diag}(\lambda(B)) U_B^{\mathsf H}$, and set $W = U_A^{\mathsf H} U_B$ (a unitary matrix). Here $\lambda_k(A)$, $\lambda_l(B)$ denote the (unsorted, Mathlib-indexed) eigenvalues eigenvalues, and $\|W_{kl}\|^2$ are the entries of the entrywise squared-norm matrix normSqMatrix W.

Statement.

That is, the real trace pairing of two Hermitian matrices is a bilinear form in their eigenvalue vectors, weighted by the doubly stochastic matrix $(\|W_{kl}\|^2)$. In the module Zeta23.LinAlg.VonNeumann this identity is the algebraic half of the proof of von Neumann's trace inequality RHLinalg.vonNeumann_trace_ineq: combining it with RHLinalg.normSqMatrix_mem_doublyStochastic_of_unitary and the rearrangement step over doubly stochastic matrices yields the bound by the sorted eigenvalue pairing.