integrableOn_Ioi_deriv_of_nonneg'

English

If f′ is nonnegative on Ioi(a) and f′ is integrable there, then the integral identity with limit holds, implying FTC-2 style results.

Русский

Если производная неотрицательна на Ioi(a) и интегрируема, то справедливо формула Фунд. теоремы.

LaTeX

$$$\\text{If } g'\\ge 0\\text{ on }Ioi(a)\\text{ and } g'\\in L^1(Ioi(a)),$ then $\\int_{Ioi(a)} g' = lim.$$$

Lean4

/-- When a function has a limit at infinity, and its derivative is nonnegative, then the derivative
is automatically integrable on `(a, +∞)`. Version assuming differentiability
on `[a, +∞)`. -/
theorem integrableOn_Ioi_deriv_of_nonneg' (hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x) (g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x)
    (hg : Tendsto g atTop (𝓝 l)) : IntegrableOn g' (Ioi a) :=
  by
  refine integrableOn_Ioi_deriv_of_nonneg ?_ (fun x hx => hderiv x hx.out.le) g'pos hg
  exact (hderiv a left_mem_Ici).continuousAt.continuousWithinAt

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