measurable_fderiv_apply_const_with_param

English

If hf is continuous in the uncurry sense, then the map p ↦ fderiv 𝕜 (f p.1) p.2 y is measurable for each fixed y ∈ E.

Русский

Если hf непрерывно в смысле uncurry, то отображение p ↦ fderiv 𝕜 (f p.1) p.2 y измеримо для каждого фиксированного y ∈ E.

LaTeX

$$$$\\Measurable (\\lambda p:\\alpha \\times E, fderiv 𝕜 (f p.1) p.2 y)$$$$

Lean4

theorem measurable_fderiv_apply_const_with_param [MeasurableSpace F] [BorelSpace F] (hf : Continuous f.uncurry)
    (y : E) : Measurable (fun (p : α × E) ↦ fderiv 𝕜 (f p.1) p.2 y) :=
  (ContinuousLinearMap.measurable_apply y).comp (measurable_fderiv_with_param 𝕜 hf)

Похожие утверждения