deriv_integral_left — Mathlib

English

There are variants that state the derivative of the right-hand endpoint map is f(b) and of the left-hand endpoint map is −f(a) when f is integrable and continuous at the appropriate endpoint.

Русский

Существуют варианты, где правая граница дает производную f(b), левая −f(a) при интегрируемости и непрерывности в границах.

LaTeX

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

Lean4

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

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