English
For a real-valued function f on a measurable set s, the lintegral over f''s equals the integral over s of |f'| times g∘f for a suitable g.
Русский
Для функции f на измеримом s справедлива линегральная формула: линеграль над образами равен интегралу по s от |f'|·g(f(x)).
LaTeX
$$$$ \\int_{f''s} g(x) \\, d\\mu = \\int_s |f'(x)| \\cdot g(f(x)) \\, d\\mu $$$$
Lean4
/-- Integrability in the change of variable formula for differentiable functions (one-variable
version): if a function `f` is injective and differentiable on a measurable set `s ⊆ ℝ`, then the
Lebesgue integral of a function `g : ℝ → ℝ≥0∞` on `f '' s` coincides with the Lebesgue integral
of `|(f' x)| * g ∘ f` on `s`. -/
theorem lintegral_image_eq_lintegral_abs_deriv_mul (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x)
(hf : InjOn f s) (g : ℝ → ℝ≥0∞) : ∫⁻ x in f '' s, g x = ∫⁻ x in s, ENNReal.ofReal (|f' x|) * g (f x) := by
simpa only [det_one_smulRight] using
lintegral_image_eq_lintegral_abs_det_fderiv_mul volume hs (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g
