English
For antitone f on s and differentiable with derivative f', the integrability of g on the image f''s is equivalent to integrability of |f'| times g∘f on s.
Русский
Для антиинвариантной f на s и дифференцируемой с производной f' интегрируемость g на образе f''s эквивалентна интегрируемости |f'|·g∘f на s.
LaTeX
$$$$ \\text{IntegrableOn } g \\ (f''s) \\iff \\text{IntegrableOn } (x \\mapsto |f'(x)| \\, g(f(x)))\\ s $$$$
Lean4
/-- 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 Bochner integral of a
function `g : ℝ → F` on `f '' s` coincides with the integral of `|(f' x)| • g ∘ f` on `s`. -/
theorem integral_image_eq_integral_abs_deriv_smul (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x)
(hf : InjOn f s) (g : ℝ → F) : ∫ x in f '' s, g x = ∫ x in s, |f' x| • g (f x) := by
simpa only [det_one_smulRight] using
integral_image_eq_integral_abs_det_fderiv_smul volume hs (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g
