aestronglyMeasurable_lineDeriv — Mathlib

English

If f is continuous, then the a.e.-strongly measurable line derivative function is AEStronglyMeasurable with respect to μ.

Русский

Если f непрерывна, то функция линейной производной является AEStronglyMeasurable по μ.

LaTeX

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

Lean4

theorem aestronglyMeasurable_lineDeriv [SecondCountableTopologyEither E F] (hf : Continuous f) (μ : Measure E) :
    AEStronglyMeasurable (fun x ↦ lineDeriv 𝕜 f x v) μ :=
  (stronglyMeasurable_lineDeriv hf).aestronglyMeasurable

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