English
Let hf be a continuous curried function f.uncurry. Then the map p ↦ fderiv 𝕜 (f p.1) p.2 is measurable on α × E.
Русский
Пусть hf — непрерывная функция, задающая зависимость через каррирование. Тогда отображение p ↦ fderiv 𝕜 (f p.1) p.2 измеримо на α × E.
LaTeX
$$$$\\Measurable (\\lambda p:\\alpha\\times E, f\\deriv 𝕜 (f p.1) p.2)$$$$
Lean4
theorem measurable_fderiv_with_param (hf : Continuous f.uncurry) :
Measurable (fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) :=
by
refine measurable_of_isClosed (fun s hs ↦ ?_)
have :
(fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s =
{p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
{p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | (0 : E →L[𝕜] F) ∈ s} :=
Set.ext (fun x ↦ mem_preimage.trans fderiv_mem_iff)
rw [this]
exact
(measurableSet_of_differentiableAt_of_isComplete_with_param hf hs.isComplete).union
((measurableSet_of_differentiableAt_with_param _ hf).compl.inter (MeasurableSet.const _))
