English
Under second-countable assumptions, the map p ↦ deriv (f p.1) p.2 is strongly measurable in p, possibly after organizing the ambient spaces.
Русский
При предположениях вторичного счётного пространства отображение p ↦ deriv (f p.1) p.2 сильно измеримо по p.
LaTeX
$$$$\\text{StronglyMeasurable }\\bigl(\\lambda p:(\\alpha\\times 𝕜), \\ deriv (f p.1) p.2\\bigr)$$$$
Lean4
theorem stronglyMeasurable_deriv_with_param [LocallyCompactSpace 𝕜] [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
[h : SecondCountableTopologyEither α F] {f : α → 𝕜 → F} (hf : Continuous f.uncurry) :
StronglyMeasurable (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) :=
by
borelize F
rcases h.out with hα | hF
· have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜
apply stronglyMeasurable_iff_measurable_separable.2 ⟨measurable_deriv_with_param hf, ?_⟩
have : range (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) ⊆ closure (Submodule.span 𝕜 (range f.uncurry)) :=
by
rintro - ⟨p, rfl⟩
have A : deriv (f p.1) p.2 ∈ closure (Submodule.span 𝕜 (range (f p.1))) :=
by
rw [← image_univ]
apply range_deriv_subset_closure_span_image _ dense_univ (mem_range_self _)
have B : range (f p.1) ⊆ range (f.uncurry) := by
rintro - ⟨x, rfl⟩
exact mem_range_self (p.1, x)
exact closure_mono (Submodule.span_mono B) A
exact (isSeparable_range hf).span.closure.mono this
· exact (measurable_deriv_with_param hf).stronglyMeasurable
