English
A change of variables formula holds for polar coordinates: integrating a function after pulling back along polarCoord.symm equals integrating the function itself over the plane.
Русский
Для полярных координат выполняется формула замены переменных: интеграл функции после обратного полярного отображения равен интегралу самой функции по плоскости.
LaTeX
$$$\int_{p \in \mathrm{polarCoord.target}} p_1 \; f(\mathrm{polarCoord.symm}(p))\, dp = \int_{p} f(p)\, dp.$$$
Lean4
protected theorem integral_comp_polarCoord_symm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℂ → E) :
(∫ p in polarCoord.target, p.1 • f (Complex.polarCoord.symm p)) = ∫ p, f p :=
by
rw [← (Complex.volume_preserving_equiv_real_prod.symm).integral_comp measurableEquivRealProd.symm.measurableEmbedding,
← integral_comp_polarCoord_symm]
simp_rw [measurableEquivRealProd_symm_polarCoord_symm_apply]
