Differential Entropy Change of Variables

Abstract

Differential entropy changes by the expected logarithm of the absolute Jacobian.

Theorem 1.1 (A differentiable equivalence contributes its log-Jacobian correction).

$$\begin{array}{c}\forall n\in \mathbb{N},p:{\mathbb{R}}^n\to \mathbb{R},\\ f:\mathrm{Equiv}({\mathbb{R}}^n,{\mathbb{R}}^n),A:{\mathbb{R}}^n\to \mathrm{ContinuousLinearMap}(\mathbb{R},{\mathbb{R}}^n,{\mathbb{R}}^n),\\ (\forall x\in {\mathbb{R}}^n,0\le p(x))\wedge \\ {\int }_{{\mathbb{R}}^n}(p(x))dx=1\wedge \\ \mathrm{Integrable}((x\mapsto p(x)\cdot \log (p(x))))\wedge \\ \mathrm{Integrable}((x\mapsto p(x)\cdot \log (|\det (A(x))|)))\wedge \\ (\forall x\in {\mathbb{R}}^n,\mathrm{HasFDerivAt}(f,A(x),x))\wedge \\ (\forall x\in {\mathbb{R}}^n,0<|\det (A(x))|)\\ \Rightarrow \mathrm{let}(J(x):=|\det (A(x))|,\\ q(y):=\frac{p(\mathrm{symm}(f,y))}{J(\mathrm{symm}(f,y))},\\ h(r):=-{\int }_{{\mathbb{R}}^n}(r(x)\cdot \log (r(x)))dx)\\ \mathrm{Integrable}((y\mapsto q(y)\cdot \log (q(y))))\wedge \\ h(q)=h(p)+{\int }_{{\mathbb{R}}^n}(p(x)\cdot \log (J(x)))dx\wedge \\ (\forall c\in \mathbb{R},0<c\Rightarrow (\forall x\in \mathrm{support}(p),J(x)=c)\Rightarrow {\int }_{{\mathbb{R}}^n}(p(x)\cdot \log (J(x)))dx=\log (c)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Relabeling/DifferentialEntropyChangeOfVariables.differential_entropy_change_of_variables (✓ std3). ∎

Source. Repository-derived.

Commentary.

The carrier is the real vector space R^n. A nonnegative unit-mass density p, a differentiable equivalence f, its derivative A, and an everywhere-positive absolute determinant construct J(x) = |det A(x)| and the transformed density q(y) = p(f^{-1}(y))/J(f^{-1}(y)).

Integrability of p log p expresses finite source differential entropy. Integrability of p log J expresses finite absolute expected log-Jacobian. The transformed entropy integrand is integrable, and h(q) equals h(p) plus the density-weighted integral of log J.

If J is the positive constant c on the support of p, normalization makes the correction exactly log c. The qualitative observation that the correction usually depends on both the map and the distribution is not universalized.

The proof directly applies Mathlib’s Jacobian change-of-variables theorem and its integrability equivalence. The remaining pointwise identity is log(p/J) = log p - log J, with the zero-density case handled separately.

References

• Truth anchor: D5/S3/Entropy/Relabeling/DifferentialEntropyChangeOfVariables.differential_entropy_change_of_variables
• Dependency: D5/S3/Entropy/Relabeling/InjectiveInvariance