English
If a function has a limit at infinity, and its derivative is nonpositive, then the integral over (−∞, a] and tail relate by a subtraction formula.
Русский
Если предел на бесконечности и производная не положительная, то интеграл на (−∞, a] связан с пределом через вычитание.
LaTeX
$$$\\int_{Iic(a)} f' = f(a) - m$ with m = limUnder atBot f.$$
Lean4
/-- When a function has a limit at infinity `l`, and its derivative is nonpositive, then the
integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see
`integrable_on_Ioi_deriv_of_nonneg`). Version assuming differentiability on `(a, +∞)` and
continuity at `a⁺`. -/
theorem integral_Ioi_of_hasDerivAt_of_nonpos (hcont : ContinuousWithinAt g (Ici a) a)
(hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x) (g'neg : ∀ x ∈ Ioi a, g' x ≤ 0) (hg : Tendsto g atTop (𝓝 l)) :
∫ x in Ioi a, g' x = l - g a :=
integral_Ioi_of_hasDerivAt_of_tendsto hcont hderiv (integrableOn_Ioi_deriv_of_nonpos hcont hderiv g'neg hg) hg
