English
In the vector-valued setting, if the derivative exists at the endpoints (HasDerivAt) and the interior derivatives exist, then ∫_a^b u(x) · v'(x) dx = u(b) · v(b) − u(a) · v(a) − ∫_a^b u'(x) · v(x) dx.
Русский
В векторном случае, если производные существуют в концах ([a,b]) и внутри, то формула по частям сохраняется: ∫_a^b u(x) · v'(x) dx = u(b) · v(b) − u(a) · v(a) − ∫_a^b u'(x) · v(x) dx.
LaTeX
$$$\\displaystyle \\int_a^b u(x) \\cdot v'(x) \\,dx = u(b) \\cdot v(b) - u(a) \\cdot v(a) - \\int_a^b u'(x) \\cdot v(x) \\,dx$$$
Lean4
/-- **Integration by parts** (vector-valued). Special case of
`intervalIntegrable.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right`
where the functions have a derivative also at the endpoints. -/
theorem integral_smul_deriv_eq_deriv_smul (hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x)
(hv : ∀ x ∈ [[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_smul_deriv_eq_deriv_smul_of_hasDerivWithinAt (fun x hx ↦ (hu x hx).hasDerivWithinAt)
(fun x hx ↦ (hv x hx).hasDerivWithinAt) hu' hv'
