aeStronglyMeasurable_mkD_restrict_of_uncurry

English

For t with CompactSpace t, if f and g are as, then x ↦ mkD (t.restrict (f x)) g is AEStronglyMeasurable.

Русский

Для t с компактным пространством, если f,g удовлетворяют условиям, то x ↦ mkD (t.restrict (f x)) g измеримо ae.

LaTeX

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

Lean4

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

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