English
Under suitable finite-measure and measurability assumptions, the mapping a ↦ κ a(t) is measurable for every measurable t, enabling a kernel-level measurability result.
Русский
При надлежащих предположениях о конечности меры и измеримости отображение a ↦ κ a(t) измеримо для каждого измеримого t, что обеспечивает измеримость на уровне ядра.
LaTeX
$$$\\text{Measurable } a \\mapsto κ(a)(t)\\quad( t \\in \\mathrm{Set})$$$
Lean4
theorem integral_kernel_prod_left'' {f : γ × β → E} (hf : StronglyMeasurable f) :
StronglyMeasurable fun y => ∫ x, f (x, y) ∂η (a, y) :=
by
change StronglyMeasurable ((fun y => ∫ x, (fun u : γ × α × β => f (u.1, u.2.2)) (x, y) ∂η y) ∘ fun x => (a, x))
apply StronglyMeasurable.comp_measurable _ (measurable_prodMk_left (m := mα))
· have :=
MeasureTheory.StronglyMeasurable.integral_kernel_prod_left' (κ := η)
(hf.comp_measurable (measurable_fst.prodMk measurable_snd.snd))
simpa using this
