integrableOn_Ioi_deriv_of_nonpos — Mathlib

English

An FTC variant with differentiability on Ioi and nonnegative derivative, giving an integral identity over Ioi.

Русский

Variant FTC на Ioi с неотрицательной производной.

LaTeX

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

Lean4

/-- When a function has a limit at infinity, and its derivative is nonpositive, then the derivative
is automatically integrable on `(a, +∞)`. Version assuming differentiability
on `(a, +∞)` and continuity at `a⁺`. -/
theorem integrableOn_Ioi_deriv_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)) :
    IntegrableOn g' (Ioi a) := by
  apply integrable_neg_iff.1
  exact
    integrableOn_Ioi_deriv_of_nonneg hcont.neg (fun x hx => (hderiv x hx).neg)
      (fun x hx => neg_nonneg_of_nonpos (g'neg x hx)) hg.neg

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