English
If u is differentiable with HasDerivWithinAt on ((a,b)) and v similarly, then the IBP identity holds for the vector-valued case with appropriate integrability assumptions.
Русский
Если u имеет HasDerivWithinAt и v аналогично, тогда векторная формула IBP выполняется под допустимыми условиями интегрируемости.
LaTeX
$$$\\displaystyle \\int_a^b u(x) \\cdot v'(x) \\,dx = u(b) \\cdot v(b) - u(a) \\cdot v(a) - \\int_a^b u'(x) \\cdot v(x) \\,dx$$$
Lean4
theorem integral_deriv_comp_smul_deriv' (hf : ContinuousOn f [[a, b]])
(hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x) (hf' : ContinuousOn f' [[a, b]])
(hg : ContinuousOn g [[f a, f b]])
(hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x)
(hg' : ContinuousOn g' (f '' [[a, b]])) : (∫ x in a..b, f' x • (g' ∘ f) x) = (g ∘ f) b - (g ∘ f) a :=
by
rw [integral_comp_smul_deriv'' hf hff' hf' hg',
integral_eq_sub_of_hasDeriv_right hg hgg' (hg'.mono _).intervalIntegrable]
exacts [rfl, intermediate_value_uIcc hf]
