English
Under appropriate differentiability assumptions with interior derivatives, the IBP formula holds for vector-valued integrals.
Русский
При подходящих предположениях о дифференцируемости с внутренними производными формула 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
/-- Change of variables, most common version. If `f` has continuous derivative `f'` on `[a, b]`,
and `g` is continuous, then we can substitute `u = f x` to get
`∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.
If the function `f` is monotone or antitone, see also
`integral_image_eq_integral_deriv_smul_of_monotoneOn` dropping all assumptions on `g`. -/
theorem integral_comp_smul_deriv (h : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x) (h' : ContinuousOn f' (uIcc a b))
(hg : Continuous g) : (∫ x in a..b, f' x • (g ∘ f) x) = ∫ x in f a..f b, g x :=
integral_comp_smul_deriv' h h' hg.continuousOn
