Kernel randomization from the uniform source on [0,1] (R4 converse piece 1, #107)

The small adapter from Mathlib's kernel representation theorem (ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval, Kallenberg Lemma 4.22) to the project's uniform source uniform01 : Measure ℝ: any Markov kernel into a standard Borel space is the pushforward of uniform01 by a jointly measurable deterministic map, and any probability measure on a standard Borel space is a pushforward of uniform01. Outside [0,1] the map factors through Set.projIcc — only measurability and agreement on the support matter.

• ProbabilityTheory.Kernel.exists_measurable_map_eq_uniform01 — the kernel form;
• MeasureTheory.Measure.exists_measurable_map_eq_uniform01 — the single-measure corollary.

This is the randomization ("noise outsourcing") input for the converse representation theorem: each regular conditional distribution along the factor filtration is to be realized as a measurable function of the lower factors and one fresh uniform.

theorem MeasureTheory.uniform01_eq_map_volume_coe : uniform01 = Measure.map Subtype.val volume

uniform01 is the pushforward of the uniform measure on the subtype I = [0,1] along the inclusion.

theorem MeasureTheory.uniform01_map_projIcc : Measure.map (Set.projIcc 0 1 ⋯) uniform01 = volume

Projecting uniform01 back onto the subtype recovers the uniform measure on I — Set.projIcc retracts the inclusion, and uniform01 is supported on [0,1].

theorem ProbabilityTheory.Kernel.exists_measurable_map_eq_uniform01 {X : Type u_1} {Y : Type u_2} {mX : MeasurableSpace X} [Nonempty Y] {mY : MeasurableSpace Y} [StandardBorelSpace Y] (κ : Kernel X Y) [IsMarkovKernel κ] : ∃ (f : X → ℝ → Y), Measurable (Function.uncurry f) ∧ ∀ (x : X), MeasureTheory.Measure.map (f x) MeasureTheory.uniform01 = κ x

Kernel randomization from uniform01: a Markov kernel into a standard Borel space is the pushforward of the project's uniform source by a jointly measurable deterministic map — Mathlib's exists_measurable_map_eq_unitInterval (Kallenberg Lemma 4.22) with the [0,1]-subtype input adapted to ℝ through Set.projIcc.

theorem MeasureTheory.Measure.exists_measurable_map_eq_uniform01 {Y : Type u_1} [Nonempty Y] {mY : MeasurableSpace Y} [StandardBorelSpace Y] (μ : Measure Y) [IsProbabilityMeasure μ] : ∃ (f : ℝ → Y), Measurable f ∧ map f uniform01 = μ

Measure randomization from uniform01: a probability measure on a standard Borel space is a pushforward of the project's uniform source by a measurable map.