English
The change of variables formula holds: the lintegral of |det f'| over s equals the measure of the image f''s.
Русский
Формула изменения переменной выполняется: линтеграл от |det f'| по s равен мере образа f''s.
LaTeX
$$$$ \int_{s} |\det f'(x)| \, d\mu = \mu(f''s). $$$$
Lean4
/-- Change of variable formula for differentiable functions, set version: if a function `f` is
injective and differentiable on a measurable set `s`, then the measure of `f '' s` is given by the
integral of `|(f' x).det|` on `s`.
Note that the measurability of `f '' s` is given by `measurable_image_of_fderivWithin`. -/
theorem lintegral_abs_det_fderiv_eq_addHaar_image (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
(hf : InjOn f s) : (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) = μ (f '' s) :=
le_antisymm (lintegral_abs_det_fderiv_le_addHaar_image μ hs hf' hf)
(addHaar_image_le_lintegral_abs_det_fderiv μ hs hf')
