English
In the Lebesgue-integral setting, for locally integrable vector-valued functions with appropriate derivatives, the integration-by-parts identity holds in a local sense on an interval.
Русский
В рамках лебеговской интеграции для локально интегрируемых векторнозначных функций с соответствующими производными локально на интервале выполняется тождество IBP.
LaTeX
$$$\\text{(local Lebesgue IBP)}\\quad \\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. If `f` has continuous derivative `f'` on `[a, b]`,
and `g` is continuous on `f '' [a, b]`, 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`.
Compared to `intervalIntegral.integral_comp_smul_deriv` we only require that `g` is continuous on
`f '' [a, b]`.
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 : ContinuousOn g (f '' [[a, b]])) : (∫ x in a..b, f' x • (g ∘ f) x) = ∫ x in f a..f b, g x :=
integral_comp_smul_deriv'' (fun x hx ↦ (h x hx).continuousAt.continuousWithinAt)
(fun x hx ↦ (h x <| Ioo_subset_Icc_self hx).hasDerivWithinAt) h' hg
