stronglyMeasurable_lineDeriv — Mathlib

English

If f is continuous, then the a.e. measurable version of the line derivative x ↦ lineDeriv 𝕜 f x v holds for any measure μ.

Русский

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

LaTeX

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

Lean4

theorem stronglyMeasurable_lineDeriv [SecondCountableTopologyEither E F] (hf : Continuous f) :
    StronglyMeasurable (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 (stronglyMeasurable_deriv_with_param hg).comp_measurable measurable_prodMk_right

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