integral_Ioi_of_hasDerivAt_of_nonpos'

English

If a function's derivative is nonpositive and integrable on Iic a, then the improper integral identity holds with −m.

Русский

Производная неотрицательна, интегрируема на Iic(a); формула интеграла с −m.

LaTeX

$$$\\int_{Iic(a)} g' x = f(a) - m$ under hypotheses.$$

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

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