integral_Ioi_of_hasDerivAt_of_nonneg'

English

A variant for the Iic tail, showing the convergence of interval integrals to the integral over Iic when the left endpoints go to −∞.

Русский

Вариант для хвоста Iic, сходящийся к интегралу на Iic при уходе левых концов к −∞.

LaTeX

$$$\\int_{Iic(a)} f' = \\lim\\_{b\\to -\\infty} \\int_{Iic(b)} f'$.$$

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, +∞)`. -/
theorem integral_Ioi_of_hasDerivAt_of_nonneg' (hderiv : ∀ x ∈ Ici 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' hderiv (integrableOn_Ioi_deriv_of_nonneg' hderiv g'pos hg) hg

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