English
A function g is integrable on the image f''s if and only if the pullback density |det f'| times g∘f is integrable on s.
Русский
Функция g интегрируема на образе f''s тогда и только тогда, когда плотность |det f'|·(g∘f) интегрируема на s.
LaTeX
$$$$ \\text{IntegrableOn } g(f''s) \\iff \\text{IntegrableOn } (x \\mapsto |\\det f'(x)| \\cdot g(f(x)))\\ s $$$$
Lean4
/-- Integrability in the change of variable formula for differentiable functions: if a
function `f` is injective and differentiable on a measurable set `s`, then a function
`g : E → F` is integrable on `f '' s` if and only if `|(f' x).det| • g ∘ f` is
integrable on `s`. -/
theorem integrableOn_image_iff_integrableOn_abs_det_fderiv_smul (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) (g : E → F) :
IntegrableOn g (f '' s) μ ↔ IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ :=
by
rw [IntegrableOn, ← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,
(measurableEmbedding_of_fderivWithin hs hf' hf).integrable_map_iff]
simp only [Set.restrict_eq, ← Function.comp_assoc, ENNReal.ofReal]
rw [← (MeasurableEmbedding.subtype_coe hs).integrable_map_iff, map_comap_subtype_coe hs, restrict_withDensity hs,
integrable_withDensity_iff_integrable_coe_smul₀]
· simp_rw [IntegrableOn, Real.coe_toNNReal _ (abs_nonneg _), Function.comp_apply]
· exact aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf'
