aestronglyMeasurable_deriv_with_param

English

If the ambient topology allows, the map p ↦ deriv (f p.1) p.2 is AEStronglyMeasurable for μ.

Русский

Если топология допускает, отображение p ↦ deriv (f p.1) p.2 является AEStronglyMeasurable по μ.

LaTeX

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

Lean4

theorem aestronglyMeasurable_deriv_with_param [LocallyCompactSpace 𝕜] [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
    [SecondCountableTopologyEither α F] {f : α → 𝕜 → F} (hf : Continuous f.uncurry) (μ : Measure (α × 𝕜)) :
    AEStronglyMeasurable (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2) μ :=
  (stronglyMeasurable_deriv_with_param hf).aestronglyMeasurable

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