Canonical Conditional Information Submodularity

Abstract

Conditional product laws make canonical selected-output information submodular.

Theorem 1.1 (Canonical selected mutual information has diminishing returns).

$$\begin{array}{c}\forall Index:\mathrm{Type},Hidden:\mathrm{Type},\\ Output:Index\to \mathrm{Type},\\ (\mathrm{Fintype}(Hidden)\wedge \forall i:Index,\mathrm{Fintype}(Output(i)))\Rightarrow \\ \forall S:\mathrm{Finset}(Index),T:\mathrm{Finset}(Index),e:Index,\\ p:(Hidden\times (\forall i:\mathrm{insert}(e,T),Output(\mathrm{val}(i))))\to \mathbb{R},\\ S\subseteq T\wedge \neg e\in T\wedge \\ ((\forall z:(Hidden\times (\forall i:\mathrm{insert}(e,T),Output(\mathrm{val}(i)))),0\le p(z))\wedge \sum _{z:(Hidden\times (\forall i:\mathrm{insert}(e,T),Output(\mathrm{val}(i))))}p(z)=1)\Rightarrow \\ \mathrm{let}{p}_S:(Hidden\times (\forall i:S,Output(\mathrm{val}(i))))\to \mathbb{R}:=\mathrm{selectedMarginal}(p,S),\\ p_{\mathrm{insert}(e,S)}:(Hidden\times (\forall i:\mathrm{insert}(e,S),Output(\mathrm{val}(i))))\to \mathbb{R}:=\mathrm{selectedMarginal}(p,\mathrm{insert}(e,S)),\\ p_T:(Hidden\times (\forall i:T,Output(\mathrm{val}(i))))\to \mathbb{R}:=\mathrm{selectedMarginal}(p,T),\\ p_{\mathrm{insert}(e,T)}:(Hidden\times (\forall i:\mathrm{insert}(e,T),Output(\mathrm{val}(i))))\to \mathbb{R}:=p,\\ p_{S,Hidden;T\setminus S,e}:(((\forall i:S,Output(\mathrm{val}(i)))\times Hidden)\times ((\forall i:T\setminus S,Output(\mathrm{val}(i)))\times Output(e)))\to \mathbb{R}:=\mathrm{canonicalContextLaw}(p,S,T,e)\\ \mathrm{in}(\forall c:((\forall i:S,Output(\mathrm{val}(i)))\times Hidden),\mathrm{marginal}(p_{S,Hidden;T\setminus S,e})(c)\ne 0\Rightarrow \mathrm{conditional}(p_{S,Hidden;T\setminus S,e},c)=(w:((\forall i:T\setminus S,Output(\mathrm{val}(i)))\times Output(e))\mapsto \mathrm{marginal}(\mathrm{conditional}(p_{S,Hidden;T\setminus S,e},c))(\mathrm{fst}(w))\times \mathrm{marginal}(\mathrm{swapLaw}(\mathrm{conditional}(p_{S,Hidden;T\setminus S,e},c)))(\mathrm{snd}(w))))\Rightarrow \\ \mathrm{mutualInformation}(p_{\mathrm{insert}(e,S)})-\mathrm{mutualInformation}(p_S)\ge \mathrm{mutualInformation}(p_{\mathrm{insert}(e,T)})-\mathrm{mutualInformation}(p_T).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Submodularity/CanonicalConditionalInformationSubmodularity.canonical_conditional_information_submodular (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let the hidden state and every output alphabet be finite. The joint mass is carried by the hidden state together with the exact dependent output tuple indexed by insert e T; the ambient index type itself need not be finite.

For S contained in T and e outside T, the canonical finite-set equivalences split the T-output tuple into the S outputs and the outputs indexed by T minus S, and split insert e T into the T outputs and the output at e.

The displayed context law is obtained from that same canonical mass. On each active context consisting of the S-output tuple and hidden state, the conditional law of the remaining T-outputs and the e output factors as the product of its two marginals.

The four explicitly typed selected marginals live on S, insert e S, T, and insert e T. Two finite mutual-information chain rules and the conditional product criterion yield the stated diminishing-return inequality.

References

• Truth anchor: D5/S3/Entropy/Submodularity/CanonicalConditionalInformationSubmodularity.canonical_conditional_information_submodular
• Dependency: D5/S3/Entropy/Submodularity/MutualInformationChainRule