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