English
Let t be a compact space with zero; f: X → Y → E, g ∈ C(t,E)₀; if f is continuous on univ × t via uncurry and f(x)(0)=0 a.e. on μ, then x ↦ mkD(t.restrict (f(x))) g is AEStronglyMeasurable w.r.t. μ.
Русский
Пусть t — компактное множество с нулём, f: X → Y → E, g ∈ C(t,E)₀; если f(x) непрерывна через uncurry на всей продукции и f(x)(0)=0 a.e., то x ↦ mkD(t.restrict (f(x))) g является AES-измеримой относительно μ.
LaTeX
$$$$\\Bigl( \\text{Compact}(t)\\land \\text{Zero}(t)\\land f: X \\to Y \\to E\\land g \\in C(t,E)_0\\land (\\text{ContinuousOn}(\\text{Function.uncurry } f)\\text{ on }\\mathrm{univ} \\times t)\\land (\\forall^{\\mu} x, f(x)(0)=0) \\Bigr) \\\\Rightarrow AEStronglyMeasurable\\bigl(x \\mapsto mkD(t.restrict (f(x)))\\,g\\bigr)\\ (\\mu) $$$$
Lean4
theorem aeStronglyMeasurable_mkD_restrict_of_uncurry {t : Set Y} [CompactSpace t] [Zero 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)) (f_zero : ∀ᵐ x ∂μ, f x (0 : t) = 0) :
AEStronglyMeasurable (fun x ↦ mkD (t.restrict (f x)) g) μ :=
by
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
refine aestronglyMeasurable_congr ?_ |>.mp <| ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry f g f_cont
filter_upwards [f_zero] with x zero_x
rw [mkD_eq_mkD_of_map_zero _ _ zero_x]
