English
For any Ω with standard Borel structure and any η : Kernel α ℝ, the borelMarkovFromReal construction provides a Markov-type kernel whose evaluation at a point a ∈ α is given by a conditional rule determined by whether η a places mass outside the image embeddingReal Ω.
Русский
Для любого Ω с стандартной бореловой структурой и η : Kernel α ℝ конструирование borelMarkovFromReal задаёт ядро типа Маркова, чьё значение в точке a определяется условно в зависимости от того, лежит ли масса η a за пределами образа embeddingReal Ω.
LaTeX
$$$\\mathrm{borelMarkovFromReal}\\,\\Omega\\,\\eta\\,a = \\begin{cases} (\\eta\\,a)\\circ(\\mathrm{embeddingReal}\\,\\Omega)^{-1}, & ((\\eta\\,a)(\\mathrm{range}(\\mathrm{embeddingReal}\\,\\Omega)))^{c}=0 \\\\[2mm] \\mathrm{dirac}_{\\mathrm{range\\_nonempty}(\\mathrm{embeddingReal}\\,\\Omega)}\\circ(\\mathrm{embeddingReal}\\,\\Omega), & \\text{otherwise} \\end{cases}$$$
Lean4
theorem borelMarkovFromReal_apply (Ω : Type*) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω] (η : Kernel α ℝ)
(a : α) :
borelMarkovFromReal Ω η a =
if η a (range (embeddingReal Ω))ᶜ = 0 then (η a).comap (embeddingReal Ω)
else (Measure.dirac (range_nonempty (embeddingReal Ω)).choose).comap (embeddingReal Ω) :=
by
classical
rw [borelMarkovFromReal, comapRight_apply, piecewise_apply, deterministic_apply]
simp only [mem_preimage, mem_singleton_iff]
split_ifs <;> rfl
