Author Information Decomposition

Abstract

Conditional action entropy splits into internal-state information and residual entropy.

Theorem 1.1 (Internal-state information decomposes conditional action entropy).

$$\begin{array}{r}\forall Public,Action,Memory:\mathrm{Type},\\ (\mathrm{Fintype}\left(Public\right)\wedge \mathrm{Fintype}\left(Action\right)\wedge \mathrm{Fintype}\left(Memory\right)),\\ jointLaw:\mathrm{Prod}\left(Public,\mathrm{Prod}\left(Action,Memory\right)\right)\to \mathbb{R},\forall z:\mathrm{Prod}\left(Public,\mathrm{Prod}\left(Action,Memory\right)\right),0\le \mathrm{jointLaw}\left(z\right)\Rightarrow \\ \mathrm{let}actionGivenPublicLaw:=\mathrm{xyProjection}\left(jointLaw\right),\\ \mathrm{let}actionGivenPublicMemoryLaw:\mathrm{Prod}\left(\mathrm{Prod}\left(Public,Memory\right),Action\right)\to \mathbb{R}:=z\mapsto \mathrm{jointLaw}\left(\mathrm{pair}\left(\mathrm{fst}\left(\mathrm{fst}\left(z\right)\right),\mathrm{pair}\left(\mathrm{snd}\left(z\right),\mathrm{snd}\left(\mathrm{fst}\left(z\right)\right)\right)\right)\right),\\ \mathrm{conditionalEntropy}\left(actionGivenPublicLaw\right)=\mathrm{conditionalMutualInformation}\left(jointLaw\right)+\mathrm{conditionalEntropy}\left(actionGivenPublicMemoryLaw\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Observation/AuthorInformationDecomposition.author_information_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let Public, Action, and Memory be arbitrary finite carriers. The nonnegative joint mass is ordered as Public times (Action times Memory), matching the conditioning coordinate used by the canonical finite entropy interface.

The public-action law is the canonical projection that sums out Memory. The action-given-public-and-memory law is constructed by reindexing the same joint mass onto (Public times Memory) times Action; it is not defined from the target equality.

Applying the entropy chain rule before and after that reindexing shows that action entropy given Public equals conditional mutual information between Action and Memory given Public, plus the action entropy remaining after Memory is also known.

The two explanatory bullets following the source’s boxed identity are interpretive labels for its summands, not additional mathematical clauses.

References

• Truth anchor: D5/S3/Entropy/Observation/AuthorInformationDecomposition.author_information_decomposition
• Dependency: D5/S3/Entropy/Submodularity/ConditionalMutualInformation