Lean4
/-- Auxiliary definition for `ProbabilityTheory.Kernel.condKernel`.
A Borel space `Ω` embeds measurably into `ℝ` (with embedding `e`), hence we can get a `Kernel α Ω`
from a `Kernel α ℝ` by taking the comap by `e`.
Here we take the comap of a modification of `η : Kernel α ℝ`, useful when `η a` is a probability
measure with all its mass on `range e` almost everywhere with respect to some measure and we want to
ensure that the comap is a Markov kernel.
We thus take the comap by `e` of a kernel defined piecewise: `η` when
`η a (range (embeddingReal Ω))ᶜ = 0`, and an arbitrary deterministic kernel otherwise. -/
noncomputable def borelMarkovFromReal (Ω : Type*) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω]
(η : Kernel α ℝ) : Kernel α Ω :=
have he := measurableEmbedding_embeddingReal Ω
let x₀ := (range_nonempty (embeddingReal Ω)).choose
comapRight
(piecewise
((Kernel.measurable_coe η he.measurableSet_range.compl) (measurableSet_singleton 0) :
MeasurableSet {a | η a (range (embeddingReal Ω))ᶜ = 0})
η (deterministic (fun _ ↦ x₀) measurable_const))
he
