English
If f has a continuous derivative f' on [a,b] and g is continuous, then ∫_a^b f'(x) (g ∘ f)(x) dx = ∫_{f(a)}^{f(b)} g(u) du.
Русский
Если f имеет непрерывную производную f' на [a,b] и g непрерывна, то ∫_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. 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, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
Compared to `intervalIntegral.integral_comp_mul_deriv` we only require that `g` is continuous on
`f '' [a, b]`.
-/
theorem integral_comp_mul_deriv' {f f' g : ℝ → ℝ} (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, (g ∘ f) x * f' x) = ∫ x in f a..f b, g x := by
simpa [mul_comm] using integral_comp_smul_deriv' h h' hg
