differentiable_integral_of_continuous

English

If f is continuous, then the function F(u) = ∫_{a}^{u} f(x) dx is differentiable on ℝ, with derivative F'(u) = f(u).

Русский

Пусть f непрерывна; тогда F(u) = ∫_{a}^{u} f(x) dx дифференцируема на ℝ и F'(u)=f(u).

LaTeX

$$$F(u)=\\int_{a}^{u} f(x)\\,dx \\quad\\Rightarrow\\quad F'(u)=f(u)\\quad(\\forall u\\in\\mathbb{R}).$$$

Lean4

/-- The integral of a continuous function is differentiable on a real set `s`. -/
theorem differentiable_integral_of_continuous (hcont : Continuous f) : Differentiable ℝ (fun u => ∫ x in a..u, f x) :=
  fun _ ↦
  (integral_hasDerivAt_right (hcont.intervalIntegrable _ _) hcont.aestronglyMeasurable.stronglyMeasurableAtFilter
      hcont.continuousAt).differentiableAt

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