Finite Deficiency Triangle

Abstract

One-way finite experiment deficiency satisfies the triangle inequality under simulator composition.

Theorem 1.1 (Finite deficiency obeys the triangle inequality).

$$\begin{array}{c}\forall Theta,X,Y,Z:Type,\\ \mathrm{Fintype}(Theta)\wedge \mathrm{Nonempty}(Theta)\wedge \mathrm{Fintype}(X)\wedge \mathrm{Fintype}(Y)\wedge \mathrm{Fintype}(Z),\\ E:\mathrm{FiniteMarkovKernel}(Theta,X),F:\mathrm{FiniteMarkovKernel}(Theta,Y),G:\mathrm{FiniteMarkovKernel}(Theta,Z)\Rightarrow \\ \mathrm{finiteDeficiency}(G,E)\le \mathrm{finiteDeficiency}(G,F)+\mathrm{finiteDeficiency}(F,E).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/SequentialDecisionRisk/FiniteDeficiencyTriangle.finite_deficiency_triangle (✓ std3). ∎

Source. Repository-derived.

Commentary.

Two row-stochastic simulators compose to a row-stochastic simulator. The total-variation triangle inequality and channel contraction bound its error, and independent infima give the stated deficiency inequality.

References

• Truth anchor: D5/S3/Estimation/SequentialDecisionRisk/FiniteDeficiencyTriangle.finite_deficiency_triangle
• Dependency: D5/S3/Estimation/SequentialDecisionRisk/FiniteDeficiencyRiskTransfer