Countable Pairwise Singular Common Partition

Abstract

Pairwise singular probability laws have a common measurable partition into full-measure supports.

Theorem 1.1 (Pairwise singular laws have disjoint full-measure supports).

$$\begin{gathered} \forall \alpha :\mathrm{Type},[\mathrm{MeasurableSpace}\left(\alpha \right)], \\ P:\mathbb{N}\to \mathrm{Measure}\left(\alpha \right),a:\mathbb{N}\to \mathrm{ENNReal}, \\ (\forall n,\mathrm{ProbabilityMeasure}\left(P_n\right))\wedge (\forall n,0<a_n)\wedge \sum _{n\in \mathbb{N}}{a}_n=1\wedge \\ (\forall n,m,n\ne m\Rightarrow \mathrm{MutuallySingular}\left(P_n,P_m\right)) \\ \Rightarrow \mathrm{let}\lambda =\sum _{n\in \mathbb{N}}{a}_n{P}_n,f=(n\mapsto \frac{\mathrm{d}{P}_n}{\mathrm{d}\lambda }) \\ (\forall n,m,n\ne m\Rightarrow f_n{f}_m=0\lambda \text{ almost everywhere})\wedge \\ \exists A:\mathbb{N}\to \mathrm{Set}\left(\alpha \right),(\forall n,\mathrm{Measurable}\left(A_n\right))\wedge \mathrm{PairwiseDisjoint}\left(A\right)\wedge \\ (\forall n,P_n(A_n)=1). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let P_n be countably many probability laws on one measurable transcript space. Positive normalized weights construct their mixture lambda, and f_n is the Radon–Nikodym derivative of P_n with respect to that mixture.

Pairwise mutual singularity forces f_n f_m to vanish lambda-almost everywhere whenever n and m differ. This is the density form of the separation claim in the source.

The nonzero density supports are measurable and pairwise disjoint up to lambda-null sets. The countable measurable refinement theorem removes those overlaps simultaneously, producing genuinely pairwise disjoint measurable sets A_n. Absolute continuity transfers the refinement equality back to every P_n, so each law assigns its own set mass one.

References

• Truth anchor: D5/S3/Observer/MeasureSeparation/CountableSingularPartition.countable_pairwise_singular_common_partition