English
A refined version of the fundamental theorem for improper integrals on a semi-infinite interval, with nonnegative derivative and integrability, showing equality of the improper integral and subtraction from a limit.
Русский
Уточнённая версия FTC для несобственного интеграла на полунеограниченном промежутке с неотрицательной производной и интегрируемостью.
LaTeX
$$$\\int_{Ioi(a)} g' x\,dx = l - g(a).$$$
Lean4
/-- When a function has a limit at infinity `l`, and its derivative is nonnegative, 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_nonneg (hcont : ContinuousWithinAt g (Ici a) a)
(hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x) (g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x) (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_nonneg hcont hderiv g'pos hg) hg
