English
The integral of the derivative of a product with right derivatives: ∫ (u v' + u' v) equals (u b)(v b) − (u a)(v a) minus ∫ u' v.
Русский
Интегрирование по частям для правых производных: ∫ (u v' + u' v) = u(b)v(b) − u(a)v(a) − ∫ u' v.
LaTeX
$$$\\int_{a}^{b} (u(x) v'(x) + u'(x) v(x))\,dx = u(b) v(b) - u(a) v(a) - \\int_{a}^{b} u'(x) v(x) \\,dx$$$
Lean4
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is differentiable at every `x` in `[a, b]` and
its derivative is integrable on `[a, b]`, then `∫ y in a..b, deriv f y` equals `f b - f a`.
See also `integral_deriv_of_contDiffOn_Icc` for a similar theorem assuming that `f` is `C^1`. -/
theorem integral_deriv_eq_sub (hderiv : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x)
(hint : IntervalIntegrable (deriv f) volume a b) : ∫ y in a..b, deriv f y = f b - f a :=
integral_eq_sub_of_hasDerivAt (fun x hx => (hderiv x hx).hasDerivAt) hint
