English
Special case using HasDerivWithinAt from endpoints for the product rule within the interval.
Русский
Особый случай с HasDerivWithinAt для окончания внутри интервала в правиле произведения.
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
one-sided derivative at the endpoints. -/
theorem integral_deriv_mul_eq_sub_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 x * v' x = u b * v b - u a * v a :=
integral_deriv_mul_eq_sub_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'
