English
If φ majorizes the derivative g' on Ioc, then ∫ φ ≥ g(b) − g(a).
Русский
Если φ верхнее обособляет производную g' на Ioc, тогда ∫ φ ≥ g(b) − g(a).
LaTeX
$$$\\int_{a}^{b} φ(y) dy \\ge g(b)-g(a)$$$
Lean4
/-- **Fundamental theorem of calculus-2**: If `f : ℝ → E` is continuous on `[a, b]` (where `a ≤ b`)
and has a right derivative at `f' x` for all `x` in `(a, b)`, and `f'` is integrable on `[a, b]`,
then `∫ y in a..b, f' y` equals `f b - f a`. -/
theorem integral_eq_sub_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn f (Icc a b))
(hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x) (f'int : IntervalIntegrable f' volume a b) :
∫ y in a..b, f' y = f b - f a :=
by
refine (NormedSpace.eq_iff_forall_dual_eq ℝ).2 fun g => ?_
rw [← g.intervalIntegral_comp_comm f'int, g.map_sub]
exact
integral_eq_sub_of_hasDeriv_right_of_le_real hab (g.continuous.comp_continuousOn hcont)
(fun x hx => g.hasFDerivAt.comp_hasDerivWithinAt x (hderiv x hx))
(g.integrable_comp ((intervalIntegrable_iff_integrableOn_Icc_of_le hab enorm_ne_top).1 f'int))
