integral_hasDerivAt_right — Mathlib

English

If f is integrable on [a,b] and continuous at b, then the derivative of u ↦ ∫_{a}^{u} f(x) dx at u = b equals f(b).

Русский

Если f интегрируема на [a,b] и непрерывна в b, то производная u ↦ ∫_{a}^{u} f(x) dx в точке u=b равна f(b).

LaTeX

$$$\\dfrac{d}{du}\\Big|_{u=b} \\int_{a}^{u} f(x) dx = f(b).$$$

Lean4

/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f` is
continuous at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b`. -/
theorem integral_hasDerivAt_right (hf : IntervalIntegrable f volume a b) (hmeas : StronglyMeasurableAtFilter f (𝓝 b))
    (hb : ContinuousAt f b) : HasDerivAt (fun u => ∫ x in a..u, f x) (f b) b :=
  (integral_hasStrictDerivAt_right hf hmeas hb).hasDerivAt

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