Atomless standard-Borel transport to the unit interval

This file proves that an atomless standard-Borel probability space is measure-preservingly isomorphic modulo null sets to the unit interval with Lebesgue measure. The real-line construction uses the cumulative distribution function and the generalized inverse already provided by MeasureTheory.Measure.quantile, then transports a standard-Borel space to ℝ by embeddingReal.

The CDF/quantile route is adapted from Cameron Freer's independent implementation in Graphon/MeasureIso.lean at commit 9f7be59fa754d260a544b4cfd83d6a5b94f7552e: https://github.com/cameronfreer/graphon/commit/9f7be59fa754d260a544b4cfd83d6a5b94f7552e. The graphon-specific packaging was removed. The original work is copyright Cameron Freer and licensed under Apache 2.0. The underlying measure-preserving equivalence is also the standard-Borel transport theorem in S. Janson, Graphons, cut norm and distance, couplings and rearrangements, Theorem A.7.

Here NullSingletonClass μ is the formal hypothesis. On a standard-Borel space it gives the atomlessness used by the CDF argument; the class itself only asserts that every singleton is null. The mod-zero isomorphism machinery it composes is TauCeti.Mod0MeasureIso; this module composes the two transports and exports the resulting theorem exists_mpModNull_equiv_unitInterval.

The atomless real-line isomorphism

The mod-zero isomorphism between an atomless standard-Borel probability space and Lebesgue measure on the unit interval is the composite of the standard-Borel transport into ℝ with the CDF/quantile transport along ℝ.

theorem MeasureTheory.Measure.exists_mpModNull_equiv_unitInterval {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] [NullSingletonClass μ] : ∃ (f : Ω → ↑unitInterval) (g : ↑unitInterval → Ω), MeasurePreserving f μ volume ∧ MeasurePreserving g volume μ ∧ (∀ᵐ (x : Ω) ∂μ, g (f x) = x) ∧ ∀ᵐ (y : ↑unitInterval), f (g y) = y

A measure-preserving map in each direction between an atomless standard-Borel probability space and the unit interval, with the two maps mutually inverse almost everywhere.