Bounded-Risk Simulator Transport

Abstract

Uniform simulation error bounds the statewise risk increase of every bounded-loss rule.

Theorem 1.1 (A total-variation simulator transports every bounded-loss decision rule).

$$\begin{array}{c}\forall X,O,R,A,\\ \mathrm{Fintype}(X),\mathrm{Nonempty}(X),\mathrm{Fintype}(O),\\ \mathrm{Fintype}(R),\mathrm{Fintype}(A),\\ K:X\to O\to \mathbb{R},L:X\to R\to \mathbb{R},\\ M:O\to R\to \mathbb{R},d:R\to A\to \mathbb{R},\\ ell:X\to A\to \mathbb{R},epsilon:\mathbb{R},\\ (\mathrm{IsRowStochastic}(K)\wedge \mathrm{IsRowStochastic}(L)\wedge \mathrm{IsRowStochastic}(M)\wedge \mathrm{IsRowStochastic}(d)\wedge \\ (\forall x:X,a:A,0\le ell(x,a)\wedge ell(x,a)\le 1)\wedge \sup (x,\mathrm{TV}(L(x),\mathrm{channelOutput}(M,K(x))))\le epsilon)\Rightarrow \\ \mathrm{let}(dK(o)(a):=\mathrm{channelOutput}(d,M(o))(a))\\ \mathrm{IsRowStochastic}(dK)\wedge \\ \forall x:X,\mathrm{sum}(a,\mathrm{channelOutput}(dK,K(x))(a)\cdot ell(x,a))\le \mathrm{sum}(a,\mathrm{channelOutput}(d,L(x))(a)\cdot ell(x,a))+epsilon.\end{array}$$

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

Source. Repository-derived.

Commentary.

The state, observation, simulated-observation, and action carriers are finite, with a nonempty state carrier. K and L are experiments, M is the simulator, and d is an arbitrary randomized decision rule based on L; all four are row-stochastic.

The transported rule is the canonical composition: after observing K, apply M and then d. Its row-stochasticity is part of the public conclusion, so the transported object is exposed rather than hidden behind an existence claim.

For every loss taking values between zero and one, the finite supremum of the rowwise total-variation simulation error bounds the increase of expected loss separately at every state.

References

• Truth anchor: D5/S3/Estimation/DecisionRisk/BoundedRiskSimulatorTransport.bounded_loss_risk_stability_of_simulator
• Dependency: D5/S3/Estimation/DecisionRisk/DescentDefectBounds