Singular Probability Laws Have Perfect Separation

Abstract

Mutually singular probability laws admit a measurable perfect separator.

Theorem 1.1 (A measurable event separates singular laws with zero error).

$$\begin{gathered} \forall Omega:\mathrm{Type},[\mathrm{MeasurableSpace}(Omega)], \\ {P}_x,P_y:\mathrm{Measure}(Omega), \\ \mathrm{ProbabilityMeasure}(P_x)\wedge \mathrm{ProbabilityMeasure}(P_y)\wedge \mathrm{MutuallySingular}(P_x,P_y) \\ \Rightarrow \exists A_{x,y}:\mathrm{Set}(Omega),\mathrm{Measurable}(A_{x,y})\wedge P_x(A_{x,y})=1\wedge P_y(A_{x,y})=0. \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The two state-indexed transcript laws are probability measures on one measurable transcript space. Their mutual singularity is the product-singular premise established immediately before the source theorem.

Mathlib’s canonical singular set is measurable, null under the first law, and has null complement under the second law. Its complement is therefore the required event.

The probability-measure instance turns nullity of the singular set into mass one for its complement. Thus the complete transcript distinguishes the two laws outside null sets.

Repository searches found only special or premise-heavier separation results. The proof applies the pinned measurable singular-set API directly.

References

• Truth anchor: D5/S3/Observer/MeasureSeparation/SingularProbabilityPerfectSeparator.mutually_singular_probability_laws_have_perfect_separator