English
In the one-variable setting, the same change of variables formula holds with the usual Lebesgue measure on the line: the lintegral over f''s equals the integral of |f'| times g∘f over the domain.
Русский
В одномерном случае формула замены переменных сохраняется: линеграль над образами равен интегралу по области от |f'|·g∘f.
LaTeX
$$$$ \\int_{f''s} g(x) dx = \\int_s |f'(x)| \\cdot g(f(x)) dx $$$$
Lean4
/-- Change of variable formula for differentiable functions, set version: if a real function `f` is
monotone and differentiable on a measurable set `s`, then the measure of `f '' s` is given by the
integral of `f' x` on `s` .
Note that the measurability of `f '' s` is given by `MeasurableSet.image_of_monotoneOn`. -/
theorem lintegral_deriv_eq_volume_image_of_monotoneOn (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : MonotoneOn f s) :
(∫⁻ x in s, ENNReal.ofReal (f' x)) = volume (f '' s) := by
simpa using (lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn hs hf' hf 1).symm
