English
If a function has a limit at infinity and its derivative is nonnegative, then the derivative is integrable on Ioi(a).
Русский
Если функция имеет предел на бесконечности и её производная неотрицательна, то производная интегрируема на Ioi(a).
LaTeX
$$$\\text{IntegrableOn}\\ g'\\ (Ioi(a))\\text{ given nonneg derivative and limit at infinity.}$$$
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, +∞)` and continuity at `a⁺`. -/
theorem integrableOn_Ioi_deriv_of_nonneg (hcont : ContinuousWithinAt g (Ici a) a)
(hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x) (g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x) (hg : Tendsto g atTop (𝓝 l)) :
IntegrableOn g' (Ioi a) :=
by
have hcont : ContinuousOn g (Ici a) := by
intro x hx
rcases hx.out.eq_or_lt with rfl | hx
· exact hcont
· exact (hderiv x hx).continuousAt.continuousWithinAt
refine integrableOn_Ioi_of_intervalIntegral_norm_tendsto (l - g a) a (fun x => ?_) tendsto_id ?_
·
exact
intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self) (fun y hy => hderiv y hy.1)
fun y hy => g'pos y hy.1
apply Tendsto.congr' _ (hg.sub_const _)
filter_upwards [Ioi_mem_atTop a] with x hx
have h'x : a ≤ id x := le_of_lt hx
calc
g x - g a = ∫ y in a..id x, g' y := by
symm
apply
intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self) fun y hy =>
hderiv y hy.1
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]
exact
intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self) (fun y hy => hderiv y hy.1)
fun y hy => g'pos y hy.1
_ = ∫ y in a..id x, ‖g' y‖ := by
simp_rw [intervalIntegral.integral_of_le h'x]
refine setIntegral_congr_fun measurableSet_Ioc fun y hy => ?_
dsimp
rw [abs_of_nonneg]
exact g'pos _ hy.1
