measurable_lineDeriv_uncurry — Mathlib

English

If f is continuous, then the map from (x, y) ∈ E × E to lineDeriv 𝕜 f x y is measurable.

Русский

Если f непрерывна, то отображение (x, y) ↦ lineDeriv 𝕜 f x y из E × E в F измеримо.

LaTeX

$$$ \\mathrm{Measurable}\\big(p \\mapsto \\mathrm{lineDeriv}_{\\mathbb{k}}(f)(p_1)(p_2)\\big)$$$

Lean4

theorem measurable_lineDeriv_uncurry [MeasurableSpace F] [BorelSpace F] (hf : Continuous f) :
    Measurable (fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2) :=
  by
  borelize 𝕜
  let g : (E × E) → 𝕜 → F := fun p t ↦ f (p.1 + t • p.2)
  have : Continuous g.uncurry :=
    hf.comp <| (continuous_fst.comp continuous_fst).add <| continuous_snd.smul (continuous_snd.comp continuous_fst)
  exact (measurable_deriv_with_param this).comp measurable_prodMk_right

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