English
If the derivative of a product is integrable on [a,b], then the integration-by-parts identity holds with two interval integrals.
Русский
Если производная произведения интегрируема на [a,b], то выполняется формула интегрирования по частям.
LaTeX
$$$\\int_{a}^{b} u' v + u v' = u(b) v(b) - u(a) v(a) - \\int_{a}^{b} u' v$$$
Lean4
/-- **Integration by parts**. Special case of `integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right`
where the functions have a two-sided derivative in the interior of the interval. -/
theorem integral_mul_deriv_eq_deriv_mul_of_hasDerivAt (hu : ContinuousOn u [[a, b]]) (hv : ContinuousOn v [[a, b]])
(huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt u (u' x) x)
(hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt v (v' x) x) (hu' : IntervalIntegrable u' volume a b)
(hv' : IntervalIntegrable v' volume a b) :
∫ x in a..b, u x * v' x = u b * v b - u a * v a - ∫ x in a..b, u' x * v x :=
integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right hu hv (fun x hx ↦ (huu' x hx).hasDerivWithinAt)
(fun x hx ↦ (hvv' x hx).hasDerivWithinAt) hu' hv'
