English
Let f be a differentiable map with right-derivative f' on (a,b) and g be integrable on f(IoI) along with suitable continuity of g. Then ∫_a^b f'(x) · (g ∘ f)(x) dx = ∫_{f(a)}^{f(b)} g(u) du, that is a general change of variables formula for integrals with a derivative inside the integrand.
Русский
Пусть f имеет правую производную f' на (a,b) и g интегрируема на образе f, тогда ∫_a^b f'(x) · (g∘f)(x) dx = ∫_{f(a)}^{f(b)} g(u) du, это общая формула замены переменных для интегралов с производной внутри.
LaTeX
$$$\\displaystyle \\int_a^b f'(x)\\, (g\\circ f)(x)\,dx = \\int_{f(a)}^{f(b)} g(u)\\,du$$$
Lean4
/-- Change of variables for continuous integrands. If `f` is continuous on `[a, b]` and has
continuous right-derivative `f'` in `(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`.
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'' (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, b]])) : (∫ x in a..b, f' x • (g ∘ f) x) = ∫ u in f a..f b, g u :=
by
refine
integral_comp_smul_deriv''' hf hff' (hg.mono <| image_mono Ioo_subset_Icc_self) ?_
(hf'.smul (hg.comp hf <| subset_preimage_image f _)).integrableOn_Icc
rw [hf.image_uIcc] at hg ⊢
exact hg.integrableOn_Icc
