aemeasurable_lineDeriv — Mathlib

English

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

Русский

Если f непрерывна, то a.e.-сильно измеримая версия линейной производной существует.

LaTeX

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

Lean4

theorem aemeasurable_lineDeriv [MeasurableSpace F] [BorelSpace F] (hf : Continuous f) (μ : Measure E) :
    AEMeasurable (fun x ↦ lineDeriv 𝕜 f x v) μ :=
  (measurable_lineDeriv hf).aemeasurable

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