aeStronglyMeasurable_restrict_mkD_of_uncurry

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

Похожие утверждения