English
If f' is nonpositive on Iic a and f has a limit, then the integral equals l minus f(a).
Русский
Если производная не положительна на Iic и предел существует, то интеграл равен l−f(a).
LaTeX
$$$\\int_{Iic(a)} g' x = l - g(a).$$$
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)` and continuity at `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 (hcont : ContinuousWithinAt f (Iic a) a)
(hderiv : ∀ x ∈ Iio 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
have hcont : ContinuousOn f (Iic 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_Iic a f'int tendsto_id) ?_
apply Tendsto.congr' _ (hf.const_sub _)
filter_upwards [Iic_mem_atBot a] with x hx
symm
apply
intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le hx (hcont.mono Icc_subset_Iic_self) fun y hy => hderiv y hy.2
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hx]
exact f'int.mono (fun y hy => hy.2) le_rfl
