Measure-preserving maps from the unit interval

Mathlib's kernel representation theorem already gives the exact measurable map needed in Janson's Theorem A.9: every probability measure on a standard Borel space is the pushforward of Lebesgue measure on I = [0,1]. This file supplies the missing MeasurePreserving packaging.

No atomlessness hypothesis is present. The private regression examples at the end instantiate the theorem for a Dirac law, a finite atomic Bernoulli law, and a mixed atomic--continuous law.

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

Janson A.9, packaged for Mathlib: every standard Borel probability space receives a measure-preserving map from the unit interval. This is a prescribed-pushforward statement; no pointwise surjectivity is claimed or needed. Atoms are allowed.

The following examples are compile-time regressions for the absence of an atomlessness hypothesis. They are deliberately private: the public theorem above is the API.