English
For a differentiable, injective map f with an appropriate domain, the integral of a function g over the target equals the integral of |det f'| times g∘f over the source.
Русский
Для дифференцируемого и инъективного отображения f с подходящим доменом интеграл функции g по целевому множеству равен интегралу от |det f'|·g∘f по исходному множеству.
LaTeX
$$$$ \\int_{\\text{target}} g(x) \\, d\\mu = \\int_{\\text{source}} |\\det f'(x)| \\cdot g(f(x)) \\, d\\mu $$$$
Lean4
/-- Change of variable formula for differentiable functions: if a function `f` is
injective and differentiable on a measurable set `s`, then the Bochner integral of a function
`g : E → F` on `f '' s` coincides with the integral of `|(f' x).det| • g ∘ f` on `s`. -/
theorem integral_image_eq_integral_abs_det_fderiv_smul (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hf : InjOn f s) (g : E → F) :
∫ x in f '' s, g x ∂μ = ∫ x in s, |(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).integral_map]
simp only [Set.restrict_apply, ← Function.comp_apply (f := g), ENNReal.ofReal]
rw [← (MeasurableEmbedding.subtype_coe hs).integral_map, map_comap_subtype_coe hs,
setIntegral_withDensity_eq_setIntegral_smul₀ (aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf') _ hs]
congr with x
rw [NNReal.smul_def, Real.coe_toNNReal _ (abs_nonneg (f' x).det)]
