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" by Olav Kallenberg, 2021.

Statements

• ProbabilityTheory.Kernel.unitInterval_representation: for a Markov kernel κ : Kernel α I, there exists a jointly measurable function f : α → I → I such that for all a : α, volume.map (f a) = κ a.

• ProbabilityTheory.Kernel.embedding_representation: for a measurable embedding g : β → I and a Markov kernel κ : Kernel α β, there exists a jointly measurable function f : α → I → β such that for all a : α, volume.map (f a) = κ a.

• ProbabilityTheory.Kernel.representation: for a Markov kernel κ : Kernel α β with β a standard Borel space, there exists a jointly measurable function f : α → I → β such that for all a : α, volume.map (f a) = κ a. This is a consequence of ProbabilityTheory.Kernel.embedding_representation and the fact that any standard Borel space can be embedded in ℝ, and then composed with unitInterval.sigmoid.

theorem ProbabilityTheory.Kernel.unitInterval_representation {α : Type u_1} [MeasurableSpace α] (κ : Kernel α ↑unitInterval) [IsMarkovKernel κ] : ∃ (f : α → ↑unitInterval → ↑unitInterval), Measurable (Function.uncurry f) ∧ ∀ (a : α), MeasureTheory.Measure.map (f a) MeasureTheory.volume = κ a

theorem ProbabilityTheory.Kernel.embedding_representation {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [Nonempty β] [MeasurableSpace β] {g : β → ↑unitInterval} (hg : MeasurableEmbedding g) (κ : Kernel α β) [IsMarkovKernel κ] : ∃ (f : α → ↑unitInterval → β), Measurable (Function.uncurry f) ∧ ∀ (a : α), MeasureTheory.Measure.map (f a) MeasureTheory.volume = κ a

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

theorem ProbabilityTheory.representation_measure {β : Type u_1} {mβ : MeasurableSpace β} [Nonempty β] [StandardBorelSpace β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure μ] : ∃ (f : ↑unitInterval → β), Measurable f ∧ MeasureTheory.Measure.map f MeasureTheory.volume = μ