English
For a measurable set s and differentiable f with injectivity on s, the lintegral over the image f''s of a function g equals the lintegral over s of |det f'| times g∘f.
Русский
Для измеримого s и дифференцируемой инъективной f на s линегральная интеграция по образу f''s функции g равна интегралу по s от |det f'|·g(f(x)).
LaTeX
$$$$ \\int_{f''s} g(x) \\, d\\mu \\\\ = \\, \\int_s |\\det f'(x)| \\cdot g(f(x)) \\, d\\mu $$$$
Lean4
theorem lintegral_image_eq_lintegral_abs_det_fderiv_mul (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) (g : E → ℝ≥0∞) :
∫⁻ x in f '' s, g x ∂μ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ :=
by
rw [← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,
(measurableEmbedding_of_fderivWithin hs hf' hf).lintegral_map]
simp only [Set.restrict_apply, ← Function.comp_apply (f := g)]
rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs,
setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
· simp only [Pi.mul_apply]
· simp only [eventually_true, ENNReal.ofReal_lt_top]
· exact aemeasurable_ofReal_abs_det_fderivWithin μ hs hf'
