Universal Belief Decision Sufficiency

Abstract

A belief identifies Bayes value simultaneously for every future decision task.

Theorem 1.1 (The belief quotient is sufficient for every Bayes decision problem).

$$\begin{array}{c}\forall X,H,P,F:Type,\\ \mathrm{MeasurableSpace}(X),\mathrm{MeasurableSpace}(F),\\ pi:H\to \mathrm{ProbabilityMeasure}(X),\\ Q:P\to \{kappa:\mathrm{Kernel}(X,F)\mid \mathrm{IsMarkovKernel}(kappa)\},\\ h,h^{\prime }:H,\\ pi(h)=pi(h^{\prime })\Rightarrow \\ \forall p:P,A:Type,\\ ell:X\to A\to ENNReal,\\ {\inf }_{d:F\to A}\mathrm{lintegral}(x,\mathrm{lintegral}(f,ell(x)(d(f)),Q(p)(x)),pi(h))={\inf }_{d:F\to A}\mathrm{lintegral}(x,\mathrm{lintegral}(f,ell(x)(d(f)),Q(p)(x)),pi(h^{\prime })).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/DataProcessing/UniversalBeliefDecisionSufficiency.task_independent_belief_sufficiency (✓ std3). ∎

Source. Repository-derived.

Commentary.

Histories map to probability measures on an arbitrary measurable hidden state. Each future policy supplies a Markov kernel from that state to a complete future transcript.

A terminal decision may depend on the entire future transcript. The displayed infimum explicitly ranges over rules d from F to A.

Equality of two history posteriors preserves this value for every policy, action carrier, and nonnegative extended-real loss simultaneously.

References

• Truth anchor: D5/S3/Estimation/DataProcessing/UniversalBeliefDecisionSufficiency.task_independent_belief_sufficiency
• Dependency: D5/S3/Estimation/SequentialDecisionRisk/TaskIndependentBeliefSufficiency