Representation of kernels

This file contains results about isolation of kernels randomness. In particular, it shows that, when the target space is a standard Borel space, any Markov kernel can be represented as the image of the uniform measure on [0,1] by a deterministic map. It corresponds to Lemma 4.22 in Foundations of Modern Probability.

Main results

• ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval: for a Markov kernel κ : Kernel X Y with Y a standard Borel space, there exists a jointly measurable function f : X → I → Y such that for all a : X, volume.map (f a) = κ a.

• ProbabilityTheory.Kernel.exists_measurable_map_eq: for a probability measure μ on a standard Borel space Y, there exists a measurable function f : I → Y such that volume.map f = μ.

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

theorem MeasureTheory.Measure.exists_measurable_map_eq {Y : Type u_2} [Nonempty Y] {mY : MeasurableSpace Y} [StandardBorelSpace Y] (μ : Measure Y) [IsProbabilityMeasure μ] : ∃ (f : ↑unitInterval → Y), Measurable f ∧ map f volume = μ