Conditional-Independent Information Submodularity

Abstract

Conditional product laws make finite selected information submodular.

Theorem 1.1 (Selected mutual information has diminishing returns).

$$\forall I\in \mathrm{Type},X\in \mathrm{Type},Y\in I\to \mathrm{Type},S\in \mathrm{Finset}\left(I\right),T\in \mathrm{Finset}\left(I\right),e\in I,p\in Y_S\times (Y_{T\setminus S}\times (X\times Y_e))\to \mathbb{R},\left(\mathrm{Finite}\left(I\right)\wedge \left(\mathrm{Fintype}\left(X\right)\wedge \left(\mathrm{Fintype}\left(Y_S\right)\wedge \left(\mathrm{Fintype}\left(Y_{T\setminus S}\right)\wedge \left(\mathrm{Fintype}\left(Y_e\right)\wedge \left(S\subseteq T\wedge \left(\left(\neg e\in T\right)\wedge \left(\left(\mathrm{Nonnegative}\left(p\right)\wedge \mathrm{totalMass}\left(p\right)=1\right)\wedge \forall (y_S,x),\mathrm{active}\left(p,(y_S,x)\right)\Rightarrow p(y_{T\setminus S},y_e\mid (y_S,x))=p(y_{T\setminus S}\mid (y_S,x))\times p(y_e\mid (y_S,x))\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow I_p(X,Y_{\mathrm{insert}\left(e,S\right)})-I_p(X,Y_S)\ge I_p(X,Y_{\mathrm{insert}\left(e,T\right)})-I_p(X,Y_T)$$

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

Source. Repository-derived.

Commentary.

A finite experiment index set carries finite dependent output types. For S contained in T and e outside T, the joint law is written on the tuple of outputs from S, the additional tuple from T minus S, the hidden state, and the output of e.

Conditional independence is stated on that joint law: at every active context consisting of the S-output tuple and hidden state, the joint conditional law of the remaining T-outputs and e factors as the product of its two marginals.

The four marginal laws constructed from the same joint mass are exactly the laws for S, S with e, T, and T with e. Their mutual-information increments satisfy the displayed diminishing-returns inequality.

The proof applies the finite mutual-information chain rule twice. The difference of conditional gains is the nonnegative conditional information between the remaining T-outputs and e given S, after the product-slice term is identified with zero.

References

• Truth anchor: D5/S3/Entropy/Submodularity/ConditionalIndependentInformationSubmodularity.conditional_independent_information_submodular
• Dependency: D5/S3/Entropy/Submodularity/MutualInformationChainRule