Finite Deficiency Risk Transfer

Abstract

One-way finite experiment deficiency bounds the increase in optimal risk for every loss in the unit interval.

Theorem 1.1 (Deficiency controls bounded-loss Bayes risk).

$$\begin{array}{c}\forall Theta,X,Y,A:Type,\\ \mathrm{Fintype}(Theta)\wedge \mathrm{Nonempty}(Theta)\wedge \mathrm{Fintype}(X)\wedge \mathrm{Fintype}(Y)\wedge \mathrm{Fintype}(A),\\ pi:Theta\to \mathbb{R},ell:Theta\to A\to \mathbb{R},E:Theta\to X\to \mathbb{R},F:Theta\to Y\to \mathbb{R},\\ (\forall theta,0\le \mathrm{apply}(pi,theta))\wedge \mathrm{sum}(pi)=1\wedge \mathrm{IsRowStochastic}(E)\wedge \mathrm{IsRowStochastic}(F),\\ (\forall theta,a,0\le \mathrm{apply}(ell,theta,a)\wedge \mathrm{apply}(ell,theta,a)\le 1)\Rightarrow \\ \mathrm{finiteBayesRisk}(pi,ell,E)\le \mathrm{finiteBayesRisk}(pi,ell,F)+\mathrm{finiteDeficiency}(F,E).\end{array}$$

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

Source. Repository-derived.

Commentary.

A target decision is transported through each source-to-target simulator. The frozen statewise total-variation bound is averaged by the prior, after which extended-nonnegative infima optimize the decision and simulator independently.

References

• Truth anchor: D5/S3/Estimation/SequentialDecisionRisk/FiniteDeficiencyRiskTransfer.deficiency_risk_bound
• Dependency: D5/S3/Estimation/DecisionRisk/BoundedRiskSimulatorTransport