English
A change-of-variables formula for integrals holds in the polar-symmetric setting: the integral over the multivariate polar target with appropriate weight equals the integral over the original domain.
Русский
Формула замены переменных для интегралов в полярной симметрии: интеграл по полярной целевой области с соответствующим весом равен интегралу по исходной области.
LaTeX
$$$\int_{p \in (\mathrm{Set.univ.pi}\; \mathrm{polarCoord.target})} (\prod_i (p_i)_1)\, f(\mathrm{polarCoord.symm}(p)) \, dp = \int_p f(p) \, dp.$$$
Lean4
theorem pi_polarCoord_symm_target_ae_eq_univ :
(Pi.map (fun _ : ι ↦ polarCoord.symm) '' Set.univ.pi fun _ ↦ polarCoord.target) =ᵐ[volume] Set.univ :=
by
rw [Set.piMap_image_univ_pi, polarCoord.symm_image_target_eq_source, volume_pi, ← Set.pi_univ]
exact ae_eq_set_pi fun _ _ ↦ polarCoord_source_ae_eq_univ
