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 trace of functional calculus is the eigenvalue sum).

$$\forall n\in \mathrm{Type},[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall A\in \mathrm{Matrix}\left(n,n,\mathbb{C}\right),\forall h\in \mathrm{IsHermitian}\left(A\right),\forall f\in (\mathbb{R}\to \mathbb{R}),\mathrm{re}\left(\mathrm{trace}\left(\mathrm{cfc}\left(f,A\right)\right)\right)=\sum _{i:n}f\left(\mathrm{eigenvalues}\left(h,i\right)\right)$$

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

Source. Repository-derived.

Commentary.

For a Hermitian complex matrix on any finite carrier and any real-valued function, the real part of the trace of its Hermitian functional calculus is the sum of the function over the matrix eigenvalues. Unitary diagonalization and cyclicity of trace give the identity.

Theorem 1.2 (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
• Truth anchor: D5/S3/Resource/LogDet/PathSpectralClassical.trace_cfc_eq_sum
• Dependency: D5/S3/Resource/LogDetDivergence