English
If f is antitone on s and differentiable with derivative f', then the lintegral over f''s of a function g equals the integral over s of |f'| times g∘f with a sign-appropriate orientation.
Русский
Если f антиинвариантна на s и дифференцируема, то линеграль по образу f''s функции g равен интегралу по s от |f'|·g(f(x)) с учетом знака.
LaTeX
$$$$ \\int_{f''s} g(x) \\, d\\mu = \\int_s |f'(x)| \\, 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 a
function `g : ℝ → F` is integrable on `f '' s` if and only if `|(f' x)| • g ∘ f` is integrable on
`s`. -/
theorem integrableOn_image_iff_integrableOn_abs_deriv_smul (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : InjOn f s) (g : ℝ → F) :
IntegrableOn g (f '' s) ↔ IntegrableOn (fun x => |f' x| • g (f x)) s := by
simpa only [det_one_smulRight] using
integrableOn_image_iff_integrableOn_abs_det_fderiv_smul volume hs (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g
