Zero Bayes Residual Criterion

Abstract

Equal-prior statistical residual vanishes exactly when the transcript laws are mutually singular.

Definition 1.1 (Statistical residual is half the common mass).

$$\begin{gathered} \forall Omega:\mathrm{Type}\left(\right),[\mathrm{MeasurableSpace}\left(Omega\right)], \\ {P}_x,P_y:\mathrm{Measure}\left(Omega\right), \\ \mathrm{statisticalResidual}\left(P_x,P_y\right)=\frac{\mathrm{measureReal}\left(\mathrm{measureInf}\left(P_x,P_y\right),univ\right)}{2}. \end{gathered}$$

Formalization. D5/S3/Observer/MeasureSeparation/ZeroBayesResidualCriterion.statisticalResidual (✓ std3).

Source. Repository-derived.

Commentary.

The infimum of two measures is their canonical common mass. For two probability laws, half of its mass on the full transcript space is the equal-prior optimal binary error, equivalently the Le Cam one-minus-total-variation formula.

Theorem 1.2 (Zero residual is equivalent to mutual singularity).

$$\begin{gathered} \forall Omega:\mathrm{Type}\left(\right),[\mathrm{MeasurableSpace}\left(Omega\right)], \\ {P}_x,P_y:\mathrm{Measure}\left(Omega\right), \\ \mathrm{ProbabilityMeasure}\left(P_x\right)\wedge \mathrm{ProbabilityMeasure}\left(P_y\right)\Rightarrow \mathrm{statisticalResidual}\left(P_x,P_y\right)=0\iff \mathrm{MutuallySingular}\left(P_x,P_y\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/MeasureSeparation/ZeroBayesResidualCriterion.statistical_residual_eq_zero_iff_mutually_singular (✓ std3). ∎

Source. Repository-derived.

Commentary.

The transcript carrier is arbitrary and both state-indexed laws are probability measures on its measurable structure.

Zero residual is zero total common mass. That is exactly a zero measure infimum, hence lattice disjointness; the pinned Mathlib equivalence identifies disjoint measures with mutually singular measures.

References

• Truth anchor: D5/S3/Observer/MeasureSeparation/ZeroBayesResidualCriterion.statisticalResidual
• Truth anchor: D5/S3/Observer/MeasureSeparation/ZeroBayesResidualCriterion.statistical_residual_eq_zero_iff_mutually_singular