English
Under general differentiability on the unit interval, the integration-by-parts identity holds for product derivatives.
Русский
При общем виде дифференцирования на единичном интервале формула интегрирования по частям для произведения сохраняется.
LaTeX
$$$\\int_{a}^{b} (u' v + u v') = u(b) v(b) - u(a) v(a) - \\int_{a}^{b} (u' v) dx$$$
Lean4
/-- **Integration by parts**. 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_of_hasDeriv_right (hu : ContinuousOn u [[a, b]]) (hv : ContinuousOn v [[a, b]])
(huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x)
(hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi 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 :=
by
rw [← integral_deriv_mul_eq_sub_of_hasDeriv_right hu hv huu' hvv' hu' hv', ← integral_sub]
· simp_rw [add_sub_cancel_left]
· exact (hu'.mul_continuousOn hv).add (hv'.continuousOn_mul hu)
· exact hu'.mul_continuousOn hv
