English
If (g ∘ f) x * f'(x) is integrable on [a,b], then ∫_a^b (g ∘ f)(x) f'(x) dx = ∫_{f(a)}^{f(b)} g(u) du.
Русский
Если (g ∘ f)(x) f'(x) интегрируемо на [a,b], тогда ∫_a^b (g ∘ f)(x) f'(x) dx = ∫_{f(a)}^{f(b)} g(u) du.
LaTeX
$$$\\displaystyle \\int_a^b (g \\circ f)(x) 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, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
-/
theorem integral_comp_mul_deriv'' {f f' g : ℝ → ℝ} (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, (g ∘ f) x * f' x) = ∫ u in f a..f b, g u := by
simpa [mul_comm] using integral_comp_smul_deriv'' hf hff' hf' hg
