English
Let a < b be real numbers and let u, v be differentiable on [a,b] with derivatives u' and v' respectively, and assume u' and v' are interval-integrable on [a,b]. Then the integral of the product u with the derivative of v over [a,b] satisfies the integration-by-parts formula: ∫_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, v обладают производными u', v' на [a, b], причём u' и v' интегрируемы по интервалу на [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)\\,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 derivative also at the endpoints.
For improper integrals, see
`MeasureTheory.integral_mul_deriv_eq_deriv_mul`,
`MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul`,
and `MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul`. -/
theorem integral_mul_deriv_eq_deriv_mul (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_mul_deriv_eq_deriv_mul_of_hasDerivWithinAt (fun x hx ↦ (hu x hx).hasDerivWithinAt)
(fun x hx ↦ (hv x hx).hasDerivWithinAt) hu' hv'
