Measurable Postprocessing Defect Contraction

Abstract

Measurable target postprocessing contracts the source-fiber defect of observable kernel laws.

Theorem 1.1 (Measurable postprocessing contracts the observable-kernel defect).

$$\begin{array}{c}\forall X,B,C:\mathrm{Type},\\ \mathrm{MeasurableSpace}\left(X\right),\mathrm{MeasurableSpace}\left(B\right),\mathrm{MeasurableSpace}\left(C\right),\\ K:\mathrm{Kernel}\left(X,X\right),q:X\to B,\\ r:B\to C,\mathrm{Measurable}\left(r\right)\Rightarrow \\ \mathrm{postprocessedObservableKernelDefect}\left(K,q,r\right)\le \mathrm{observableKernelDefect}\left(K,q\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

The event-supremum total-variation distance is constructed directly from measures. Each observable law is the corresponding row of K mapped through q, and the postprocessed law maps that measure through r.

For every measurable event in C, measurability of r identifies its probability after mapping with the probability of the measurable preimage event in B. The associated directed gap is therefore one of the terms in the original event supremum.

The pointwise contraction is applied to every pair of source states with the same q-value and then lifted through the outer supremum. The proof uses pinned Mathlib’s kernel and measure map computation rules.

References

• Truth anchor: D5/S3/Estimation/DataProcessing/MeasurablePostprocessingDefectContraction.measurable_postprocessing_defect_le