English
A general integration-by-parts identity for interval integrable functions with HasDerivAt derivatives; the boundary terms appear on the right-hand side.
Русский
Обобщённая формула интегрирования по частям для функций, интегрируемых на интервале, с производными на границах.
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
/-- **Integration by parts**. Special case of
`intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right`
where the functions have a one-sided derivative at the endpoints. -/
theorem integral_mul_deriv_eq_deriv_mul_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_mul_deriv_eq_deriv_mul_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'
