English
Under a general change of variables f with right-derivative, the integral of f' x • (g ∘ f) x over [a,b] equals ∫ g over [f a, f b] with corresponding boundary term.
Русский
При замене переменной f с правой производной интеграл f' x • (g ∘ f)(x) по [a,b] равен ∫ g над [f a, f b] плюс граничный член.
LaTeX
$$$\\displaystyle \\int_a^b f'(x) \\cdot (g \\circ f)(x) \\,dx = \\int_{f(a)}^{f(b)} g(u) \\,du$$$
Lean4
/-- Change of variables, general form for scalar functions. If `f` is continuous on `[a, b]` and has
continuous right-derivative `f'` in `(a, b)`, `g` is continuous on `f '' (a, b)` and integrable on
`f '' [a, b]`, and `(g ∘ f) x * f' x` is integrable on `[a, b]`, then we can substitute `u = f x`
to get `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
-/
theorem integral_comp_mul_deriv''' {a b : ℝ} {f f' : ℝ → ℝ} {g : ℝ → ℝ} (hf : ContinuousOn f [[a, b]])
(hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x)
(hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))) (hg1 : IntegrableOn g (f '' [[a, b]]))
(hg2 : IntegrableOn (fun x ↦ (g ∘ f) x * f' x) [[a, b]]) : (∫ x in a..b, (g ∘ f) x * f' x) = ∫ u in f a..f b, g u :=
by
have hg2' : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]] := by simpa [mul_comm] using hg2
simpa [mul_comm] using integral_comp_smul_deriv''' hf hff' hg_cont hg1 hg2'
