deriv_integral_of_tendsto_ae_right

English

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

Русский

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

LaTeX

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

Lean4

/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` has a finite
limit `c` almost surely at `b`, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `c`. -/
theorem deriv_integral_of_tendsto_ae_right (hf : IntervalIntegrable f volume a b)
    (hmeas : StronglyMeasurableAtFilter f (𝓝 b)) (hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 c)) :
    deriv (fun u => ∫ x in a..u, f x) b = c :=
  (integral_hasDerivAt_of_tendsto_ae_right hf hmeas hb).deriv

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