Realizing a probability law by a map from the unit interval

Every standard Borel probability space (Ω, μ) receives a measure-preserving map from (I, volume): there is f : I → Ω with volume.map f = μ. This is Theorem A.9 of Janson's Graphons, cut norm and distance, couplings and rearrangements.

Atoms are allowed. No atomless hypothesis appears, and none is needed: the statement is an existence claim about a map into Ω, not a bijection, so a law concentrated on finitely many points is realized by a step function on I. The regressions below pin this down at a Dirac mass, at a finite mixture, and at a mixture of an atom with a continuous part — the cases where an atomless reading of the theorem would fail.

This is the transport underlying the Layer 5 identification of coupling cut distance with the classical measure-preserving-map infimum: every coupling, being itself standard Borel, is realized by a pair of such maps. That identification is not proved here.

Main results

• MeasureTheory.Measure.exists_measurePreserving_from_unitInterval — a measure-preserving f : I → Ω realizing any standard-Borel probability law.

Implementation

Mathlib's MeasureTheory.Measure.exists_measurable_map_eq already supplies the function and the pushforward identity; the content here is packaging them as MeasurePreserving, which is definitionally that pair. Mathlib states it with [Nonempty Ω], which is not carried here: a probability measure on Ω already forces Ω to be nonempty, and nonempty_of_isProbabilityMeasure supplies the instance inside the proof.

References

• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Theorem A.9.
• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 5 — the (I, volume) transport target. The atomless mod-null equivalence exists_mpModNull_equiv_unitInterval and the map form cutDistPullback are separate targets and are not built here.

theorem MeasureTheory.Measure.exists_measurePreserving_from_unitInterval {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] : ∃ (f : ↑unitInterval → Ω), MeasurePreserving f volume μ

Janson A.9. Every standard Borel probability space receives a measure-preserving map from the unit interval with Lebesgue measure.

No atomless hypothesis is needed: μ may be a Dirac mass, a finite mixture, or a mixture of atoms with a continuous part.

Regressions: the atomic cases

exists_measurePreserving_from_unitInterval is stated without an atomless hypothesis. These three instantiations are what that buys, and they fail for any formulation that quietly assumes μ has no atoms.