integrableOn_Ioi_deriv_of_nonpos'

English

If a function has a limit at infinity and its derivative is nonpositive, then the derivative is integrable on Ioi(a) and the integral identity holds.

Русский

Если предел есть и производная неотрицательна, то интегрируема производная и формула интеграла.

LaTeX

$$$\\text{IntegrableOn}\\ g'\\ (Ioi(a))$ and $\\int_{Ioi(a)} g' = l - g(a)$.$$

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, +∞)`. -/
theorem integrableOn_Ioi_deriv_of_nonpos' (hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x) (g'neg : ∀ x ∈ Ioi a, g' x ≤ 0)
    (hg : Tendsto g atTop (𝓝 l)) : IntegrableOn g' (Ioi a) :=
  by
  refine integrableOn_Ioi_deriv_of_nonpos ?_ (fun x hx ↦ hderiv x hx.out.le) g'neg hg
  exact (hderiv a left_mem_Ici).continuousAt.continuousWithinAt

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