English
If u is differentiable with HasDerivWithinAt u (u' x) on (a,b) and v differentiable with HasDerivWithinAt v (v' x) on (a,b), then ∫_a^b u(x) · v'(x) + u'(x) · v(x) dx = u(b) · v(b) − u(a) · v(a).
Русский
Если u и v дифференцируемы внутри интервала и имеют производные внутри (a,b), то формула по частям для векторного умножения: ∫_a^b u(x) · v'(x) + u'(x) · v(x) dx = u(b) · v(b) − u(a) · v(a).
LaTeX
$$$\\displaystyle \\int_a^b u(x) \\cdot v'(x) + u'(x) \\cdot v(x) \, dx = u(b)\\cdot v(b) - u(a)\\cdot v(a)$$$
Lean4
/-- **Integration by parts** (vector-valued). Special case of
`intervalIntegrable.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right`
where the functions have a one-sided derivative at the endpoints. -/
theorem integral_smul_deriv_eq_deriv_smul_of_hasDerivWithinAt
(hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x)
(hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] 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_hasDerivAt (fun x hx ↦ (hu x hx).continuousWithinAt)
(fun x hx ↦ (hv x hx).continuousWithinAt)
(fun x hx ↦ hu x (mem_Icc_of_Ioo hx) |>.hasDerivAt (Icc_mem_nhds hx.1 hx.2))
(fun x hx ↦ hv x (mem_Icc_of_Ioo hx) |>.hasDerivAt (Icc_mem_nhds hx.1 hx.2)) hu' hv'
