English
Let Y be a compact space with a distinguished zero element and let E be a normed additively structured space. Suppose f: X → Y → E is such that its uncurry is continuous and f(x)(0) = 0 for μ-almost every x. Then the map x ↦ mkD(f(x)) with a fixed g ∈ C(Y,E)₀ is AEStronglyMeasurable with respect to μ.
Русский
Пусть Y — компактное множество с выбранной точкой нуля и E — нормированное аддитивное пространство. Пусть f: X → Y → E таково, что некоррентно f̃ (развернутая карта) непрерывна, и для μ-почти всех x верно f(x)(0) = 0. Тогда отображение x ↦ mkD(f(x)) с фиксированным g ∈ C(Y,E)₀ является AES-измеримо относительно μ.
LaTeX
$$$$\\text{If } Y \\text{ is compact with a distinguished } 0 \\in Y,\\; E \\text{ is a normed additively structured space,\\\\ f: X \\to Y \\to E,\\; \\text{uncurry}(f) \\text{ is continuous},\\; f(x)(0)=0 \\text{ for a.e. } x,\\\\ \\text{and } g \\in C(Y,E)_0,\\text{ then } x \\mapsto \\mathrm{mkD}(f(x))\\,g \\text{ is AEStronglyMeasurable w.r.t. } \\mu. $$$$
Lean4
theorem aeStronglyMeasurable_mkD_of_uncurry [CompactSpace Y] [Zero Y] [TopologicalSpace X] [OpensMeasurableSpace X]
[SecondCountableTopologyEither X (C(Y, E))] (f : X → Y → E) (g : C(Y, E)₀)
(f_cont : Continuous (Function.uncurry f)) (f_zero : ∀ᵐ x ∂μ, f x 0 = 0) :
AEStronglyMeasurable (fun x ↦ mkD (f x) g) μ :=
by
rw [← ContinuousMapZero.isEmbedding_toContinuousMap.aestronglyMeasurable_comp_iff]
refine aestronglyMeasurable_congr ?_ |>.mp <| ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry f g f_cont
filter_upwards [f_zero] with x zero_x
rw [mkD_eq_mkD_of_map_zero _ _ zero_x]
