English
A variant of the fundamental theorem of calculus for (a, ∞) with differentiability on [a, ∞).
Русский
Вариант фунд. теоремы исчисления на (a, ∞) при дифференцируемости на [a, ∞).
LaTeX
$$$\\int_{a}^{\\infty} f'(x)\\,dx = m - f(a) \\quad \\text{under appropriate hypotheses}.$$$
Lean4
/-- **Fundamental theorem of calculus-2**, on semi-infinite intervals `(a, +∞)`.
When a function has a limit at infinity `m`, and its derivative is integrable, then the
integral of the derivative on `(a, +∞)` is `m - f a`. Version assuming differentiability
on `[a, +∞)`.
Note that such a function always has a limit at infinity,
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi`. -/
theorem integral_Ioi_of_hasDerivAt_of_tendsto' (hderiv : ∀ x ∈ Ici a, HasDerivAt f (f' x) x)
(f'int : IntegrableOn f' (Ioi a)) (hf : Tendsto f atTop (𝓝 m)) : ∫ x in Ioi a, f' x = m - f a :=
by
refine integral_Ioi_of_hasDerivAt_of_tendsto ?_ (fun x hx => hderiv x hx.out.le) f'int hf
exact (hderiv a left_mem_Ici).continuousAt.continuousWithinAt
