English
A variant of tendsto for integrals over Iic with differentiable function and integrable derivative.
Русский
Variant tendsto для интегралов по Iic с дифференцируемой функцией.
LaTeX
$$$\\text{integral\\_Iic\\_of\\_hasDerivAt\\_of\\tendsto'}(hderiv, f'int, hf) : ∫ x \\in Iic a, f' x = f(a) - m$.$$
Lean4
/-- **Fundamental theorem of calculus-2**, on semi-infinite intervals `(-∞, a)`.
When a function has a limit `m` at `-∞`, and its derivative is integrable, then the
integral of the derivative on `(-∞, a)` is `f a - m`. Version assuming differentiability
on `(-∞, a]`.
Note that such a function always has a limit at minus infinity,
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic`. -/
theorem integral_Iic_of_hasDerivAt_of_tendsto' (hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x)
(f'int : IntegrableOn f' (Iic a)) (hf : Tendsto f atBot (𝓝 m)) : ∫ x in Iic a, f' x = f a - m :=
by
refine integral_Iic_of_hasDerivAt_of_tendsto ?_ (fun x hx => hderiv x hx.out.le) f'int hf
exact (hderiv a right_mem_Iic).continuousAt.continuousWithinAt
