Prediction Sufficiency Implies Decision Sufficiency

Abstract

A sufficient predictive readout determines expected losses and optimal actions.

Theorem 1.1 (Prediction sufficiency implies decision sufficiency).

$$\begin{array}{c}\forall X,C,Y,A:\mathrm{Type},\\ K:X\to \mathrm{PMF}(Y),CReadout:X\to C,\\ \ell :A\to Y\to \mathbb{R},\\ \mathrm{MeasurableSpace}(Y)\wedge \mathrm{MeasurableSingletonClass}(Y)\wedge \\ (\forall x:X,a:A,\mathrm{Integrable}(\ell \left(a\right),\mathrm{toMeasure}(K\left(x\right)))),\\ \forall x:X,a:A,\mathrm{expectedLoss}(K,\ell )\left(x,a\right):={\int }_Y\ell \left(a,y\right)dK\left(x\right),\\ \forall x:X,\mathrm{optimalActions}(K,\ell )\left(x\right):={\mathrm{argmin}}_{a\in A}\mathrm{expectedLoss}(K,\ell )\left(x,a\right),\\ \mathrm{Refines}(K,CReadout)\Rightarrow \\ \mathrm{Refines}(\mathrm{expectedLoss}(K,\ell ),CReadout)\wedge \mathrm{Refines}(\mathrm{optimalActions}(K,\ell ),CReadout).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Decision/PredictionDecisionSufficiency.prediction_sufficiency_implies_decision_sufficiency (✓ std3). ∎

Source. Repository-derived.

Commentary.

The outcome carrier has discrete measurable points, and every displayed action loss is integrable under every predicted law.

Expected loss is the integral of the supplied loss against the same PMF readout appearing in the refinement premise. The optimal-action readout is the full argmin set of that expected-loss profile.

Composing both constructions with the prediction factor map proves the two refinement clauses simultaneously.

References

• Truth anchor: D5/S3/ConceptDynamics/Decision/PredictionDecisionSufficiency.prediction_sufficiency_implies_decision_sufficiency
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal