deriv_integral — Mathlib

English

If f is interval-integrable on [a,b] with limits ca, cb at a and b (ae), then HasFDerivAt F(a,b) with derivative L(h,k) = k cb − h ca.

Русский

Если f интегрируема на [a,b] и пределы ca, cb существуют (ae), то характеристическая производная HasFDerivAt F в (a,b) равна L(h,k)=k cb − h ca.

LaTeX

$$$F(u,v)=\\int_{u}^{v} f(x)\\,dx,\\ HasFDerivAt F (a,b) L,\\ L(h,k)=k c_b - h c_a.$$$

Lean4

/-- **Fundamental theorem of calculus-1**, derivative in the right endpoint.

If `f : ℝ → E` is continuous, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` is `f b`. -/
theorem _root_.Continuous.deriv_integral (f : ℝ → E) (hf : Continuous f) (a b : ℝ) :
    deriv (fun u => ∫ x : ℝ in a..u, f x) b = f b :=
  (hf.integral_hasStrictDerivAt a b).hasDerivAt.deriv

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