English
A variant of borelMarkovFromReal with a measurable set s shows the pullback of s under embeddingReal Ω gives the value of the kernel on s in the two-case disintegration formula.
Русский
Вариант borelMarkovFromReal с измеримой областью s показывает, как значение ядра на s определяется через предобраз образа embeddingReal Ω в двухчленном виде дизинтеграции.
LaTeX
$$$\\mathrm{borelMarkovFromReal\\_apply'}(\\Omega\\,\\eta\\,a\\,s) = \\begin{cases} \\eta\\,a(\\mathrm{embeddingReal}\\,\\Omega\\,''s), & \\text{если условие выполняется} \\\\[2mm] (\\mathrm{embeddingReal}\\,\\Omega\\,''s)\\text{ содержит }\\,0, & \\text{иначе} \\mathbf{1}_{(\\mathrm{range\\_nonempty}(\\mathrm{embeddingReal}\\,\\Omega))}\\choose_s \\end{cases}$$$
Lean4
theorem borelMarkovFromReal_apply' (Ω : Type*) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω] (η : Kernel α ℝ)
(a : α) {s : Set Ω} (hs : MeasurableSet s) :
borelMarkovFromReal Ω η a s =
if η a (range (embeddingReal Ω))ᶜ = 0 then η a (embeddingReal Ω '' s)
else (embeddingReal Ω '' s).indicator 1 (range_nonempty (embeddingReal Ω)).choose :=
by
have he := measurableEmbedding_embeddingReal Ω
rw [borelMarkovFromReal_apply]
split_ifs with h
· rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs]
· rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs, Measure.dirac_apply]
