aestronglyMeasurable_lineDeriv_uncurry

English

For continuous f, the a.e. strong measurability of the uncurry line derivative holds with respect to any measure μ.

Русский

Для непрерывной функции f верно, что нестрогое измерение линии производной после разложения остаётся почти наверняка измеримым относительно любой меры μ.

LaTeX

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

Lean4

theorem aestronglyMeasurable_lineDeriv_uncurry (hf : Continuous f) (μ : Measure (E × E)) :
    AEStronglyMeasurable (fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2) μ :=
  (stronglyMeasurable_lineDeriv_uncurry hf).aestronglyMeasurable

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