Posterior Equality, Recovery, and Permutation Channels

Abstract

Zero data-processing defect is characterized by posterior agreement and Bayesian recovery, and it vanishes for permutation channels.

The three clauses are stated together: posterior equality on every positive output, exact recovery by the Bayesian reverse channel, and zero defect for every finite permutation channel.

Theorem 1.1 (Zero defect, recovery, and permutation equality).

$$\begin{array}{c}\forall X,Y[\mathrm{Fintype}(X)][\mathrm{Fintype}(Y)],\\ \forall p,q:X\to \mathbb{R},W:X\to Y\to \mathbb{R},\\ ((\forall x:X,0\le p(x))\wedge \sum _{x}p(x)=1)\Rightarrow \\ ((\forall x:X,0\le q(x))\wedge \sum _{x}q(x)=1)\Rightarrow \\ (\forall x:X,q(x)=0\Rightarrow p(x)=0)\Rightarrow \\ ((\forall x:X,y:Y,0\le W(x,y))\wedge (\forall x:X,\sum _{y}W(x,y)=1))\Rightarrow \\ [(D(p\Vert \Vert q)-D((Wp)\Vert \Vert (Wq))=0\iff \forall y,(Wp)(y)=0\vee {\hat{p}}_y={\hat{q}}_y)\wedge \\ (D(p\Vert \Vert q)-D((Wp)\Vert \Vert (Wq))=0\iff \exists R:Y\to X\to \mathbb{R},\\ (\forall y,x,R(y,x)=\{\begin{array}{ll}q(x),& (Wq)(y)=0\\ {\hat{q}}_y(x),& \text{otherwise}\end{array})\wedge \\ (\forall y,x,0\le R(y,x))\wedge (\forall y,\sum _{x}R(y,x)=1)\wedge \\ (R(Wp))=p\wedge (R(Wq))=q)\wedge \\ \forall e:X\equiv Y,D(p\Vert \Vert q)-D((P_{e}p)\Vert \Vert (P_{e}q))=0].\end{array}$$

Proof. Machine-checked in Lean as D5/S3/DivergenceSupport/Equality/PetzClassicalCorollary.zero_defect_equivalences_and_permutation_channel (✓ std3). ∎

Source. Repository-derived.

Commentary.

The posterior and recovery equivalences are imported exact results. For a permutation channel, the output law is the input law reindexed by the inverse equivalence. Mathlib’s finite-sum reindexing theorem then makes the two divergences equal.

References

• Truth anchor: D5/S3/DivergenceSupport/Equality/PetzClassicalCorollary.zero_defect_equivalences_and_permutation_channel
• Dependency: D5/S3/DivergenceSupport/Equality/PetzRecovery