English
Let s ⊆ X, t ⊆ Y with appropriate compactness. If f: X → Y → E is continuous on Set × Set with a.e. f(x,0)=0 on μ.restrict s, then x ↦ mkD(t.restrict (f(x))) g is AEStronglyMeasurable on μ.restrict s.
Русский
Пусть s ⊆ X, t ⊆ Y при определённых условия; если f: X → Y → E непрерывна на Set × Set и a.e. выполняется f(x,0)=0 относительно μ.restrict s, то x ↦ mkD(t.restrict (f(x))) g является AES-измеримой относительно μ.restrict s.
LaTeX
$$$$\\Bigl( s \\subset X,\\ t \\subset Y,\\; \\text{contOn}(\\text{Function.uncurry } f)\\text{ на }s \\times t,\\; (\\forall^{\\mu.restrict s} x, f(x)(0)=0) \\Bigr) \\\\Rightarrow AEStronglyMeasurable\\bigl(x \\mapsto mkD(t.restrict (f(x)))\\,g\\bigr)\\ (\\mu.restrict s) $$$$
Lean4
theorem aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry {s : Set X} {t : Set Y} [CompactSpace t] [Zero 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))
(f_zero : ∀ᵐ x ∂(μ.restrict s), f x (0 : t) = 0) :
AEStronglyMeasurable (fun x ↦ mkD (t.restrict (f x)) g) (μ.restrict s) :=
by
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
refine
aestronglyMeasurable_congr ?_ |>.mp <|
ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry hs f g f_cont
filter_upwards [f_zero] with x zero_x
rw [mkD_eq_mkD_of_map_zero _ _ zero_x]
