English
Let E be a finite-dimensional real vector space and f: E → E be differentiable on a measurable set s with injective derivative almost everywhere on s. Then the setwise change of variables formula holds: the integral of the density |det f'(x)| over s equals the Haar measure of the image f''s.
Русский
Пусть E — конечномерное вещественное векторное пространство, функция f: E → E дифференцируема на измеримой области s и производная по каждой точке x ∈ s инъективна почти везде на s. Тогда формула замены переменной: интеграл по s плотности |det f'(x)| равен мере Хаара образа f(s).
LaTeX
$$$$ \\displaystyle \\int_s |\\det f'(x)| \\, d\\mu(x) \\\\ = \\, \\mu(f''s) $$$$
Lean4
/-- Change of variable formula for differentiable functions, set version: if a function `f` is
injective and differentiable on a null measurable set `s`, then the measure of `f '' s` is given
by the integral of `|(f' x).det|` on `s`.
Note that the null-measurability of `f '' s` is given by `nullMeasurable_image_of_fderivWithin`. -/
theorem lintegral_abs_det_fderiv_eq_addHaar_image₀ (hs : NullMeasurableSet s μ)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :
(∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) = μ (f '' s) :=
by
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩
have A : μ (f '' s) = μ (f '' t) := by
apply measure_congr
have : s = t ∪ (s \ t) := by simp [union_eq_self_of_subset_left ts]
rw [this, image_union]
refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)
apply addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero _ (fun x hx ↦ ?_) (ae_eq_set.1 t_eq_s).2
exact (hf' x hx.1).differentiableWithinAt.mono diff_subset
have B : (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) = (∫⁻ x in t, ENNReal.ofReal |(f' x).det| ∂μ) :=
setLIntegral_congr t_eq_s.symm
rw [A, B, lintegral_abs_det_fderiv_eq_addHaar_image _ ht _ (hf.mono ts)]
intro x hx
exact (hf' x (ts hx)).mono ts
