English
Let hcont be continuity near a, hderiv a has derivative f', and f' integrable on Ioi(a). If f tends to m at infinity, then ∫_a^∞ f'(x) dx = m − f(a).
Русский
Пусть hcont обозначает непрерывность near a, hderiv задаёт производную f', и f' интегрируема на Ioi(a). Если f сходится к m на бесконечности, то интеграл от f' по (a, ∞) равен m − f(a).
LaTeX
$$$\\int_{a}^{\\infty} f'(x)\\,dx = m - f(a).$$$
Lean4
/-- **Fundamental theorem of calculus-2**, on semi-infinite intervals `(a, +∞)`.
When a function has a limit at infinity `m`, and its derivative is integrable, then the
integral of the derivative on `(a, +∞)` is `m - f a`. Version assuming differentiability
on `(a, +∞)` and continuity at `a⁺`.
Note that such a function always has a limit at infinity,
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi`. -/
theorem integral_Ioi_of_hasDerivAt_of_tendsto (hcont : ContinuousWithinAt f (Ici a) a)
(hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x) (f'int : IntegrableOn f' (Ioi a)) (hf : Tendsto f atTop (𝓝 m)) :
∫ x in Ioi a, f' x = m - f a :=
by
have hcont : ContinuousOn f (Ici a) := by
intro x hx
rcases hx.out.eq_or_lt with rfl | hx
· exact hcont
· exact (hderiv x hx).continuousAt.continuousWithinAt
refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi a f'int tendsto_id) ?_
apply Tendsto.congr' _ (hf.sub_const _)
filter_upwards [Ioi_mem_atTop a] with x hx
have h'x : a ≤ id x := le_of_lt hx
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 f'int.mono (fun y hy => hy.1) le_rfl
