Posterior History Compression

Abstract

The posterior measure compresses history for prediction and continuation decisions.

Theorem 1.1 (The posterior determines every future decision quantity).

$$\begin{array}{c}\forall X,H,I,E,P,A:Type,\\ \mathrm{MeasurableSpace}\left(X\right),\\ pi:H\to \mathrm{Measure}\left(X\right),\\ Q:I\to E\to X\to ENNReal,\\ C:P\to X\to ENNReal,\\ L:A\to X\to ENNReal,\\ h,h^{\prime }:H,pi(h)=pi(h^{\prime })\Rightarrow \\ (\forall i:I,e:E,\mathrm{lintegral}\left(x,Q(i)(e)(x),pi(h)\right)=\mathrm{lintegral}\left(x,Q(i)(e)(x),pi(h^{\prime })\right))\\ \wedge \\ \inf \left(a,\mathrm{lintegral}\left(x,L(a)(x),pi(h)\right)\right)=\inf \left(a,\mathrm{lintegral}\left(x,L(a)(x),pi(h^{\prime })\right)\right)\\ \wedge \\ (\forall p:P,\mathrm{lintegral}\left(x,C(p)(x),pi(h)\right)=\mathrm{lintegral}\left(x,C(p)(x),pi(h^{\prime })\right))\\ \wedge \\ \inf \left(p,\mathrm{lintegral}\left(x,C(p)(x),pi(h)\right)\right)=\inf \left(p,\mathrm{lintegral}\left(x,C(p)(x),pi(h^{\prime })\right)\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

Histories are mapped to posterior measures on an arbitrary measurable hidden-state carrier. Future event probabilities depend on a hidden state and selected experiment, never directly on history.

A loss family constructs Bayes risk by taking the infimum of posterior expected losses. A continuation policy likewise has a posterior expected cost, and the optimal continuation value is the infimum over all such policies.

The four displayed conclusions separately expose prediction, Bayes risk, every policy cost, and optimal continuation value. Equality of the posterior measures identifies each construction.

References

• Truth anchor: D5/S3/Estimation/DecisionRisk/PosteriorHistoryCompression.posterior_history_compression