aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry

English

A variant with s and t and power of equivalence; if continuity holds, ae strong measurability of mkD restricted.

Русский

Вариант с ограничениями на s и t; при условии непрерывности — ae измеримость mkD.

LaTeX

$$$\text{AEStronglyMeasurable}(x \mapsto \mathrm{mkD}(t.restrict(f x)) g, μ).$$$

Lean4

theorem aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry {s : Set X} {t : Set Y} [CompactSpace t]
    [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X (C(t, E))] (hs : MeasurableSet s)
    (f : X → Y → E) (g : C(t, E)) (f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)) :
    AEStronglyMeasurable (fun x ↦ mkD (t.restrict (f x)) g) (μ.restrict s) :=
  continuousOn_mkD_restrict_of_uncurry _ _ f_cont |>.aestronglyMeasurable hs

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