English
For u, v with right derivatives on [a,b], the integral of u(x) v'(x) + u'(x) v(x) equals u(b) v(b) − u(a) v(a) minus ∫ u'(x) v(x).
Русский
Для функций u, v с правыми производными на [a,b] выполняется равенство интеграла производной произведения: ∫ (u v' + u' v) = u(b) v(b) − u(a) v(a) − ∫ u' v.
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
/-- The integral of the derivative of a product of two maps.
Special case of `integral_deriv_mul_eq_sub_of_hasDeriv_right` where the functions have a
two-sided derivative in the interior of the interval. -/
theorem integral_deriv_mul_eq_sub_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 x * v' x = u b * v b - u a * v a :=
integral_deriv_mul_eq_sub_of_hasDeriv_right hu hv (fun x hx ↦ huu' x hx |>.hasDerivWithinAt)
(fun x hx ↦ hvv' x hx |>.hasDerivWithinAt) hu' hv'
