measurable_lineDeriv — Mathlib

English

If f is continuous, then the function x ↦ lineDeriv 𝕜 f x v is measurable (with respect to a suitable σ-algebra).

Русский

Если f непрерывна, то функция x ↦ lineDeriv 𝕜 f x v измерима относительно соответствующей сигма-алгебры.

LaTeX

$$$$ \text{Measurable }(x \mapsto \mathrm{lineDeriv}_{\mathbb{K}} f x v) $$$$

Lean4

theorem measurable_lineDeriv [MeasurableSpace F] [BorelSpace F] (hf : Continuous f) :
    Measurable (fun x ↦ lineDeriv 𝕜 f x v) := by
  borelize 𝕜
  let g : E → 𝕜 → F := fun x t ↦ f (x + t • v)
  have hg : Continuous g.uncurry := by fun_prop
  exact (measurable_deriv_with_param hg).comp measurable_prodMk_right

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