Closed form of the multivariate Gaussian KL divergence (M3b). For positive-definite covariances S₁, S₂, KL(N(m₁,S₁) ‖ N(m₂,S₂)) = ½ ( log(det S₂ / det S₁) + tr(S₂⁻¹ S₁) + ⟪m₁-m₂, S₂⁻¹(m₁-m₂)⟫ - d ).
The whitening reduction (klDivReal_multivariateGaussian_whiten) sends the pair to a KL against the standard Gaussian (klDivReal_multivariateGaussian_stdGaussian); the three scalar invariants of the whitened covariance (det_whitened, trace_whitened, normSq_cfcSqrt_inv_apply) then identify the arguments.
DeclProbabilityTheory.klDivReal_multivariateGaussian
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (m₁ m₂ : EuclideanSpace ℝ ι) {S₁ S₂ : Matrix ι ι ℝ},
S₁.PosDef →
S₂.PosDef →
InformationTheory.klDivReal (ProbabilityTheory.multivariateGaussian m₁ S₁)
(ProbabilityTheory.multivariateGaussian m₂ S₂) =
1 / 2 *
(Real.log (S₂.det / S₁.det) + (S₂⁻¹ * S₁).trace + (m₁ - m₂).ofLp ⬝ᵥ S₂⁻¹.mulVec (m₁.ofLp - m₂.ofLp) -
↑(Fintype.card ι))TopicInformation theory
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6022 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6022
Cite
Verification
- Library
- ZPM.InformationTheory.KullbackLeibler.Gaussian.ClosedForm
- Statement digest
- 4fa2e8b7b96b
- First verified
- 2026-09-24T00:00:00Z