English
A polar-coordinate version of the integral formula holds for ENNReal-valued functions: the integral over polarCoord.target with weight p.1 equals the integral over the whole domain.
Русский
Полярная версия интегральной формулы справедлива для функций, принимающих значения в ENNReal: интеграл по polarCoord.target с весом p.1 равен интегралу по всей области.
LaTeX
$$$\int_{p \in \mathrm{polarCoord.target}} \! (p_1) \cdot f(\mathrm{polarCoord.symm}(p)) \, dp = \int_{p} f(p) \, dp.$$$
Lean4
protected theorem lintegral_comp_polarCoord_symm (f : ℂ → ℝ≥0∞) :
(∫⁻ p in polarCoord.target, ENNReal.ofReal p.1 • f (Complex.polarCoord.symm p)) = ∫⁻ p, f p :=
by
rw [← (volume_preserving_equiv_real_prod.symm).lintegral_comp_emb measurableEquivRealProd.symm.measurableEmbedding, ←
lintegral_comp_polarCoord_symm]
simp_rw [measurableEquivRealProd_symm_polarCoord_symm_apply]
