Information theory

Pinsker's inequality with the sharp constant, and the Gaussian divergence in closed form.

• MTH.C-2026-6022ProbabilityTheory.klDivReal_multivariateGaussian

  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 ).

• MTH.C-2026-6024InformationTheory.pinsker_proof

  Pinsker's inequality with the sharp constant. tvDistReal P Q ≤ sqrt(klDivReal P Q / 2) for probability measures P ≪ Q with finite KL divergence.