deriv_integral_right — Mathlib

English

If f is interval-integrable on [a,b], continuous at a and b, then the derivative of F(u,v) = ∫_u^v f(x) dx at (a,b) equals the linear map (h,k) ↦ k f(b) − h f(a).

Русский

Если f интегрируема на [a,b] и непрерывна в концах, то dF_{(a,b)}(h,k) = k f(b) − h f(a).

LaTeX

$$$dF_{(a,b)}(h,k) = k f(b) - h f(a).$$$

Lean4

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

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