Quotient-Fiber Entropy Decomposition

Abstract

A finite source law splits into quotient entropy and weighted normalized-fiber entropy.

Theorem 1.1 (Finite source entropy splits over quotient fibers).

$$\begin{array}{c}\forall X,B,\mathrm{Finite}\left(X\right)\wedge \mathrm{Finite}\left(B\right),\\ p:X\to \mathbb{R},q:X\to B,\\ \mathrm{nonnegative}\left(p\right)\wedge \sum _{x}p(x)=1\Rightarrow \\ H\left(p\right)=H\left(\mathrm{push}\left(q,p\right)\right)+\sum _{b\in B}\mathrm{push}\left(q,p\right)(b)H\left(\mathrm{conditional}\left(\mathrm{push}\left(x\mapsto \mathrm{pair}\left(q(x),x\right),p\right),b\right)\right)\wedge \\ H\left(p\right)=H\left(\mathrm{push}\left(q,p\right)\right)+\mathrm{Hcond}\left(\mathrm{push}\left(x\mapsto \mathrm{pair}\left(q(x),x\right),p\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Fusion/QuotientFiberDecomposition.quotient_fiber_entropy_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let X and B be finite, let p be a nonnegative normalized mass on X, and let q map X to B. The quotient law is the deterministic pushforward of p along q.

The graph map sends x to (q(x),x). Conditioning its pushforward at b constructs the normalized source law on the fiber over b, with zero contribution when the quotient mass at b vanishes.

The first equality exposes the quotient-mass-weighted fiber sum. The second exposes the same decomposition through the canonical conditional-entropy aggregate. Injectivity of the graph map identifies graph-law entropy with source entropy, after which the finite Shannon chain rule supplies both conclusions.

References

• Truth anchor: D5/S3/Entropy/Fusion/QuotientFiberDecomposition.quotient_fiber_entropy_decomposition
• Dependency: D5/S3/Entropy/Forgetting/DeterministicEntropyEquality