Path and Spectral Forms of the Log-Determinant Divergence

Abstract

The log-determinant divergence has matching path, spectral, geometric-kernel, and classical forms.

Theorem 1.1 (The log-det divergence has path, spectral, kernel, and classical forms).

$$\begin{array}{c}n\in \mathbb{N},\rho ,\sigma \in M_n(\mathbb{C}),\mathrm{PosDef}(\rho )\wedge \mathrm{PosDef}(\sigma )⟶\\ (\mathrm{logDetDivergence}(\rho ,\sigma )={\int }_0^1(1-s)\Re \mathrm{tr}((m_s^{-1}\Delta {)}^2)ds,m_s=(1-s)\sigma +s\rho ,\Delta =\rho -\sigma )\wedge \\ (\mathrm{logDetDivergence}(\rho ,\sigma )=\sum _{i}h({\Lambda }_i),({\Lambda }_i{)}_i=\mathrm{spec}({\sigma }^{-\frac{1}{2}}\rho {\sigma }^{-\frac{1}{2}}),h(t)=t-\log (t)-1)\wedge \\ (\forall a,b>0,\frac{1}{ab}=(\frac{k_G(a,b)}{2}{)}^2,k_G(a,b)=\frac{2}{\sqrt{ab}})\wedge \\ (\forall p,q\in {\mathbb{R}}^n,(\forall i,0<p_i\wedge 0<q_i)⟶\mathrm{logDetDivergence}(\mathrm{diag}(p),\mathrm{diag}(q))=\sum _i(\frac{p_i}{q_i}-\log (\frac{p_i}{q_i})-1))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Resource/LogDet/PathSpectralClassical.log_det_path_spectral_classical (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive-definite complex matrices, the divergence is the weighted trace energy along their affine segment. Congruence by the inverse positive square root of sigma gives a positive-definite relative matrix whose eigenvalues yield the same divergence through the profile h(t) = t - log(t) - 1.

For positive scalar arguments, the reciprocal-product kernel is exactly the square of half the geometric kernel. Restricting the matrices to positive real diagonals gives the coordinatewise Itakura-Saito sum.

The proof derives the scalar integral by an explicit antiderivative, uses Hermitian functional calculus for the matrix path, and applies the trace and determinant eigenvalue formulas for the spectral form.

References

• Truth anchor: D5/S3/Resource/LogDet/PathSpectralClassical.log_det_path_spectral_classical
• Dependency: D5/S3/Resource/LogDetDivergence