English
Under HasDerivAt assumptions at the right endpoints, the integration-by-parts identity for vector-valued functions holds: ∫_a^b u(x) · v'(x) dx = u(b) · v(b) − u(a) · v(a) − ∫_a^b u'(x) · v(x) dx.
Русский
При условии существования производной в правых концах интервала векторные интегралы по частям выполняются: ∫_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 `integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right`
where the functions have a two-sided derivative in the interior of the interval. -/
theorem integral_smul_deriv_eq_deriv_smul_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_smul_deriv_eq_deriv_smul_of_hasDeriv_right hu hv (fun x hx ↦ (huu' x hx).hasDerivWithinAt)
(fun x hx ↦ (hvv' x hx).hasDerivWithinAt) hu' hv'
