Expected Posterior Entropy Reduction

Abstract

Finite experiment information gain is exactly expected posterior entropy reduction.

Theorem 1.1 (Information gain equals expected posterior entropy reduction).

$$\forall X\in Type,Y\in Type,pi\in X\to Real,W\in X\to \left(Y\to Real\right),\left(\left(\mathrm{Fintype}\left(X\right)\wedge \mathrm{Fintype}\left(Y\right)\right)\wedge \left(\left(\forall y\in Y,x\in X,0\le pi\left(x\right)\cdot W\left(x,y\right)\right)\wedge \left(\forall x\in X,\sum _{y}W\left(x,y\right)=1\right)\right)\right)\Rightarrow \mathrm{informationGain}\left(W,pi\right)=\mathrm{shannonEntropy}\left(pi\right)-\mathrm{expectedPosteriorEntropy}\left(W,pi\right)$$

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

Source. Repository-derived.

Commentary.

The state and observation carriers are finite. The induced joint weights are nonnegative, and each channel row has total mass one.

The information gain is mutual information of the observation-first joint law. The posterior is the repository’s totalized Bayes posterior, weighted by the output marginal.

Prior normalization is not needed for this finite algebraic identity. Empty carriers and zero-probability output slices are included.

Theorem 1.2 (Joint nonnegativity is necessary).

$$\begin{gathered} \mathrm{let}pi:\mathrm{Option}\left(Bool\right)\to Real:=(x\mapsto \mathrm{if}\left(x=none,-2,1\right)); \\ \mathrm{let}W:\mathrm{Option}\left(Bool\right)\to \left(Unit\to Real\right):=(x,y\mapsto 1); \\ \left(\forall x\in \mathrm{Option}\left(Bool\right),\sum _{y}W\left(x,y\right)=1\right)\wedge \left(\left(\neg \left(\forall y\in Unit,x\in \mathrm{Option}\left(Bool\right),0\le pi\left(x\right)\cdot W\left(x,y\right)\right)\right)\wedge \mathrm{informationGain}\left(W,pi\right)\ne \mathrm{shannonEntropy}\left(pi\right)-\mathrm{expectedPosteriorEntropy}\left(W,pi\right)\right) \end{gathered}$$

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

Source. Repository-derived.

Commentary.

A three-state signed prior with masses minus two, one, and one is observed through a normalized singleton-output channel.

The induced joint has a negative cell and zero output mass. Under the repository’s totalized logarithm and division conventions, the entropy-reduction identity fails.

Theorem 1.3 (Channel normalization is necessary).

$$\begin{gathered} \mathrm{let}pi:Unit\to Real:=(x\mapsto 1); \\ \mathrm{let}W:Unit\to \left(Unit\to Real\right):=(x,y\mapsto 2); \\ \left(\forall y\in Unit,x\in Unit,0\le pi\left(x\right)\cdot W\left(x,y\right)\right)\wedge \left(\left(\neg \left(\forall x\in Unit,\sum _{y}W\left(x,y\right)=1\right)\right)\wedge \mathrm{informationGain}\left(W,pi\right)\ne \mathrm{shannonEntropy}\left(pi\right)-\mathrm{expectedPosteriorEntropy}\left(W,pi\right)\right) \end{gathered}$$

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

Source. Repository-derived.

Commentary.

A singleton prior of mass one and a singleton channel row of mass two give nonnegative induced joint weights.

The row is not normalized, and its mutual information is nonzero under the repository definition while both displayed entropy terms vanish.

References

• Truth anchor: D5/S3/Entropy/Observation/ExpectedPosteriorEntropyReduction.channel_normalization_is_necessary
• Truth anchor: D5/S3/Entropy/Observation/ExpectedPosteriorEntropyReduction.information_gain_eq_expected_entropy_reduction
• Truth anchor: D5/S3/Entropy/Observation/ExpectedPosteriorEntropyReduction.joint_nonnegativity_is_necessary
• Dependency: D5/S3/Entropy/ConditionalEntropy
• Dependency: D5/S3/Entropy/MutualInformationEntropy