English
If f is injective and differentiable on a measurable set s, the pushforward of the measure μ restricted to s with density |det f'| gives the measure μ restricted to the image f''s.
Русский
Если f инъективна и дифференцируема на измеримом множестве s, образующая мера через f имеет плотность |det f'|; сдвиг меры по f на s дает меру, ограниченную образом f(s).
LaTeX
$$$$ \\mathrm{map}_f\\bigl( \\mu\\restriction s \\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 null measurable set `s`, then the pushforward of the measure with
density `|(f' x).det|` on `s` is the Lebesgue measure on the image set. -/
theorem map_withDensity_abs_det_fderiv_eq_addHaar (hs : NullMeasurableSet s μ)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) :
Measure.map f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) = μ.restrict (f '' s) :=
by
have h'f : AEMeasurable f (μ.restrict s) :=
by
apply ContinuousOn.aemeasurable₀ (fun x hx ↦ ?_) hs
exact (hf' x hx).differentiableWithinAt.continuousWithinAt
have h''f : AEMeasurable f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) :=
by
apply h'f.mono_ac
exact withDensity_absolutelyContinuous _ _
apply Measure.ext fun t ht => ?_
have h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s) := h'f.nullMeasurableSet_preimage ht
rw [map_apply_of_aemeasurable h''f ht, withDensity_apply₀ _ h't, Measure.restrict_apply ht, restrict_restrict₀ h't,
lintegral_abs_det_fderiv_eq_addHaar_image₀ μ ((nullMeasurableSet_restrict hs).1 h't)
(fun x hx => (hf' x hx.2).mono inter_subset_right) (hf.mono inter_subset_right),
image_preimage_inter]
