English
For a measurable set s and an injective differentiable map f on s, the restricted change of variables holds on the image f''s when density |det f'| is used.
Русский
Для измеримого множества s и инъективного отображения f на s справедлива ограниченная формула замены переменных с плотностью |det f'| на образе f(s).
LaTeX
$$$$ \\text{map}(s\\restriction f)\\bigl(\\text{comap}(\\cdot)(\\mu\\text{ withDensity } |\\det f'|)\\bigr) = \\mu\\restriction (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 pushforward of the measure with
density `|(f' x).det|` on `s` is the Lebesgue measure on the image set. This version is expressed
in terms of the restricted function `s.restrict f`.
For a version for the original function, see `map_withDensity_abs_det_fderiv_eq_addHaar`.
-/
theorem restrict_map_withDensity_abs_det_fderiv_eq_addHaar (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :
Measure.map (s.restrict f) (comap (↑) (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s) :=
by
obtain ⟨u, u_meas, uf⟩ : ∃ u, Measurable u ∧ EqOn u f s := by
classical
refine ⟨piecewise s f 0, ?_, piecewise_eqOn _ _ _⟩
refine ContinuousOn.measurable_piecewise ?_ continuous_zero.continuousOn hs
have : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
exact this.continuousOn
have u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x := fun x hx => (hf' x hx).congr (fun y hy => uf hy) (uf hx)
set F : s → E := u ∘ (↑) with hF
have A : Measure.map F (comap (↑) (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (u '' s) :=
by
rw [hF, ← Measure.map_map u_meas measurable_subtype_coe, map_comap_subtype_coe hs, restrict_withDensity hs]
exact map_withDensity_abs_det_fderiv_eq_addHaar μ hs.nullMeasurableSet u' (hf.congr uf.symm)
rw [uf.image_eq] at A
have : F = s.restrict f := by
ext x
exact uf x.2
rwa [this] at A
