English
An integral equality holds under the polar coordinate change between target and the whole plane via the derivative of polarCoord.symm.
Русский
Сохранение интеграла при переходе в полярные координаты через производную обратной карты поляр координат.
LaTeX
$$$$ \int_{p \in \mathrm{polarCoord.target}} p.1 \; f(\mathrm{polarCoord.symm}(p)) \, dp \,=\; \int_{q \in \mathbb{R}^2} f(q) \, dq. $$$$
Lean4
theorem integral_comp_polarCoord_symm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ × ℝ → E) :
(∫ p in polarCoord.target, p.1 • f (polarCoord.symm p)) = ∫ p, f p :=
by
symm
calc
∫ p, f p = ∫ p in polarCoord.source, f p := by
rw [← setIntegral_univ]
apply setIntegral_congr_set
exact polarCoord_source_ae_eq_univ.symm
_ = ∫ p in polarCoord.target, |p.1| • f (polarCoord.symm p) :=
by
rw [← OpenPartialHomeomorph.symm_target,
integral_target_eq_integral_abs_det_fderiv_smul volume (fun p _ ↦ hasFDerivAt_polarCoord_symm p),
OpenPartialHomeomorph.symm_source]
simp_rw [det_fderivPolarCoordSymm]
_ = ∫ p in polarCoord.target, p.1 • f (polarCoord.symm p) :=
by
apply setIntegral_congr_fun polarCoord.open_target.measurableSet fun x hx => ?_
rw [abs_of_pos hx.1]
