English
In the scalar case, for a real-valued function f and a vector-valued function g, the substitution formula holds for the integral of (g ∘ f) times f'. Specifically: ∫_{Ioi a} f'(x) g(f(x)) dx = ∫_{Ioi (f(a))} g(u) du.
Русский
Для скалярного случая существует формула замены переменной для произведения: ∫_{Ioi a} f'(x) g(f(x)) dx = ∫_{Ioi (f(a))} g(u) du.
LaTeX
$$$$ \int_{x \in Ioi a} f'(x) \cdot (g \circ f)(x) \, dx = \int_{u \in Ioi (f(a))} g(u) \, du. $$$$
Lean4
/-- Change-of-variables formula for `Ioi` integrals of scalar-valued functions -/
theorem integral_comp_mul_deriv_Ioi {f f' : ℝ → ℝ} {g : ℝ → ℝ} {a : ℝ} (hf : ContinuousOn f <| Ici a)
(hft : Tendsto f atTop atTop) (hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x)
(hg_cont : ContinuousOn g <| f '' Ioi a) (hg1 : IntegrableOn g <| f '' Ici a)
(hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a)) :
(∫ x in Ioi a, (g ∘ f) x * f' x) = ∫ u in Ioi (f a), g u :=
by
have hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) := by simpa [mul_comm] using hg2
simpa [mul_comm] using integral_comp_smul_deriv_Ioi hf hft hff' hg_cont hg1 hg2'
