Transport from atomless standard Borel spaces

An atomless standard Borel probability space admits a measurable map with any prescribed standard Borel probability law. The source is measure-preservingly mapped to the unit interval by MeasureTheory.Measure.exists_mpModNull_equiv_unitInterval, and the requested law is realized from that interval by MeasureTheory.Measure.exists_measurePreserving_from_unitInterval. The resulting map may collapse sets of positive measure when the target has atoms.

Normalization extends this to finite measures of equal mass, including zero mass when the target is nonempty. On a countable measurable source partition, one measurable map can simultaneously realize a prescribed law of matching mass on each cell.

This is the nonatomic feasibility result for the Monge transport problem. It also supplies the map realization needed when approximating couplings by graph plans.

See S. Janson, Graphons, cut norm and distance, couplings and rearrangements, Theorems A.7 and A.9, for the two standard Borel transport results being composed.

theorem MeasureTheory.Measure.exists_measurePreserving_of_nullSingleton {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] (μ : Measure X) [IsProbabilityMeasure μ] [NullSingletonClass μ] (ν : Measure Y) [IsProbabilityMeasure ν] : ∃ (T : X → Y), MeasurePreserving T μ ν

Every probability law on a standard Borel target is the image of an atomless standard Borel probability law under a measurable map. The target may have atoms.

Mathlib's Measure.exists_measurable_map_eq starts from the unit interval; the atomless source is mapped to that interval first.

theorem MeasureTheory.Measure.exists_measurePreserving_of_nullSingleton_of_measure_univ_eq {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] (μ : Measure X) [IsFiniteMeasure μ] [NullSingletonClass μ] (ν : Measure Y) (h : μ Set.univ = ν Set.univ) : ∃ (T : X → Y), MeasurePreserving T μ ν

An atomless finite measure on a standard Borel space can be mapped measurably to any standard Borel measure of the same total mass. The nonempty target permits a map even when both measures vanish.

theorem MeasureTheory.Measure.exists_measurePreserving_sum_of_nullSingleton {X : Type u_1} {Y : Type u_2} {ι : Type u_3} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] [Countable ι] (μ : Measure X) [IsFiniteMeasure μ] [NullSingletonClass μ] {A : ι → Set X} (hAm : ∀ (i : ι), MeasurableSet (A i)) (hAd : Pairwise (Function.onFun Disjoint A)) (hAu : ⋃ (i : ι), A i = Set.univ) (ν : ι → Measure Y) (hmass : ∀ (i : ι), μ (A i) = (ν i) Set.univ) : ∃ (T : X → Y), MeasurePreserving T μ (sum ν) ∧ ∀ (i : ι), MeasurePreserving T (μ.restrict (A i)) (ν i)

Realize prescribed laws cell by cell on a countable measurable partition of an atomless finite standard Borel measure. Each cell has the total mass of its prescribed law. One measurable map simultaneously realizes all these laws, and their sum is its full image law.