stronglyMeasurable_deriv — Mathlib

English

The derivative deriv f is strongly measurable under certain topological assumptions.

Русский

Производная deriv f является сильно измеримой при некоторых топологических предположениях.

LaTeX

$$$$\text{StronglyMeasurable}(\text{deriv } f).$$$$

Lean4

theorem stronglyMeasurable_deriv [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜] [h : SecondCountableTopologyEither 𝕜 F]
    (f : 𝕜 → F) : StronglyMeasurable (deriv f) := by
  borelize F
  rcases h.out with h𝕜 | hF
  · exact stronglyMeasurable_iff_measurable_separable.2 ⟨measurable_deriv f, isSeparable_range_deriv _⟩
  · exact (measurable_deriv f).stronglyMeasurable

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