English
If s is a measurable set and the restriction of uncurry f to s×univ is continuous, then x ↦ mkD(f(x)) g is AEStronglyMeasurable w.r.t μ.restrict s.
Русский
Если s измеримо и ограничение uncurry f на s×univ непрерывно, то x ↦ mkD(f(x)) g измеримо ae по μ.restrict s.
LaTeX
$$$\text{AEStronglyMeasurable}(x \mapsto \mathrm{mkD}(f(x)) g, μ\restriction s).$$$
Lean4
theorem aeStronglyMeasurable_restrict_mkD_of_uncurry [CompactSpace Y] {s : Set X} [TopologicalSpace X]
[OpensMeasurableSpace X] [SecondCountableTopologyEither X (C(Y, E))] (hs : MeasurableSet s) (f : X → Y → E)
(g : C(Y, E)) (f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)) :
AEStronglyMeasurable (fun x ↦ mkD (f x) g) (μ.restrict s) :=
continuousOn_mkD_of_uncurry _ _ f_cont |>.aestronglyMeasurable hs