aemeasurable_deriv_with_param — Mathlib

English

Under the same hypotheses, the function p ↦ deriv (f p.1) p.2 is AEStronglyMeasurable with respect to μ.

Русский

При тех же предположениях функция p ↦ deriv (f p.1) p.2 является AEStronglyMeasurable по отношению к μ.

LaTeX

$$$$\\AEStronglyMeasurable (\\lambda p:(\\alpha\\times 𝕜), \\ deriv (f p.1) p.2) \\; μ$$$$

Lean4

theorem aemeasurable_deriv_with_param [LocallyCompactSpace 𝕜] [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
    [MeasurableSpace F] [BorelSpace F] {f : α → 𝕜 → F} (hf : Continuous f.uncurry) (μ : Measure (α × 𝕜)) :
    AEMeasurable (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) μ :=
  (measurable_deriv_with_param hf).aemeasurable

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