Measurable Deficiency Triangle

Abstract

One-way deficiency of arbitrary measurable statistical experiments satisfies the triangle inequality under Markov simulator composition.

Theorem 1.1 (Measurable experiment deficiency obeys the triangle inequality).

$$\begin{array}{c}\forall Theta,X,Y,Z:\mathrm{Type},\\ \mathrm{MeasurableSpace}\left(Theta\right),\mathrm{MeasurableSpace}\left(X\right),\mathrm{MeasurableSpace}\left(Y\right),\mathrm{MeasurableSpace}\left(Z\right),\\ E:\mathrm{Kernel}\left(Theta,X\right),\mathrm{IsMarkovKernel}\left(E\right),\\ F:\mathrm{Kernel}\left(Theta,Y\right),\mathrm{IsMarkovKernel}\left(F\right),\\ G:\mathrm{Kernel}\left(Theta,Z\right),\mathrm{IsMarkovKernel}\left(G\right)\Rightarrow \\ \mathrm{measurableDeficiency}\left(G,E\right)\le \mathrm{measurableDeficiency}\left(G,F\right)+\mathrm{measurableDeficiency}\left(F,E\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

The one-way deficiency is constructed as the infimum over Markov simulators of the supremum, over parameter states, of measurable-event total variation.

Two simulators compose. The measure-level triangle inequality separates their errors, while a layer-cake argument proves that applying the second Markov kernel contracts total variation. The pointwise estimate then passes through the supremum and the two independent infima.

References

• Truth anchor: D5/S3/Estimation/SequentialDecisionRisk/MeasurableDeficiencyTriangle.measurable_deficiency_triangle
• Dependency: D5/S3/Estimation/DataProcessing/MeasurablePostprocessingDefectContraction