Finite Bayes-Risk Dominance Criterion

Abstract

Exact randomized postprocessing between finite experiments is equivalent to real Bayes-risk dominance for every finite decision problem.

Theorem 1.1 (Decision dominance characterizes finite postprocessing).

$$\begin{gathered} \begin{array}{c}\forall Theta,X,Y:Type,\\ \mathrm{Fintype}(Theta)\wedge \mathrm{Nonempty}(Theta)\wedge \mathrm{Fintype}(X)\wedge \mathrm{Fintype}(Y),\\ E:Theta\to X\to \mathbb{R},F:Theta\to Y\to \mathbb{R},\\ \mathrm{IsRowStochastic}(E)\wedge \mathrm{IsRowStochastic}(F)\Rightarrow \\ (\exists K:\mathrm{FiniteMarkovKernel}(X,Y),F=(theta\mapsto \mathrm{channelOutput}(K,E(theta))))\iff \\ (\forall A:Type,\mathrm{Fintype}(A), \\ pi:Theta\to \mathbb{R},ell:Theta\to A\to \mathbb{R}, \\ (\forall theta,0\le pi(theta))\wedge \mathrm{sum}(pi)=1\Rightarrow \\ \mathrm{sInf}(\mathrm{range}((d:\mathrm{FiniteMarkovKernel}(X,A)\mapsto \mathrm{finiteBayesCost}(pi,ell,E,d))))\le \mathrm{sInf}(\mathrm{range}((d:\mathrm{FiniteMarkovKernel}(Y,A)\mapsto \mathrm{finiteBayesCost}(pi,ell,F,d))))).\end{array} \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/DecisionRisk/FiniteBayesRiskDominanceCriterion.finite_bayes_risk_dominance_iff_postprocessing (✓ std3). ∎

Source. Repository-derived.

Commentary.

A source observation can simulate every target decision whenever a row-stochastic source-to-target kernel reproduces the target experiment. Composing that kernel with a target decision rule gives the corresponding source decision rule at the same real expected cost. The displayed risk is the real infimum of these costs, so negative losses are retained rather than truncated.

Conversely, the finite product of row simplexes is compact and convex. A target outside its simulated image has a strict linear separator; a uniform prior and shifted real loss turn that separator into a finite decision problem that reverses the asserted risk order.

References

• Truth anchor: D5/S3/Estimation/DecisionRisk/FiniteBayesRiskDominanceCriterion.finite_bayes_risk_dominance_iff_postprocessing
• Dependency: D5/S3/Estimation/SequentialDecisionRisk/FiniteDeficiencyRiskTransfer