English
For a finite index set ι, the lintegral over the universal pi-space with polar coordinates satisfies a change-of-variables formula: the left-hand side equals the right-hand side after transporting via polar coordinates and multiplying by the appropriate product of first coordinates.
Русский
Для конечного множества ι, линеграл над пространством с полярными координатами удовлетворяет формуле смены переменных: левая часть равна правой после переносa через полярные координаты и умножения на произведение первых координат.
LaTeX
$$$\\\\int^{-}_{p \\in (Set.univ.\\\\pi (polarCoord.target))} \\\\left( \\\\prod_{i} .ofReal (p i).1 \\right) \\\\; f (polarCoord.symm p) \\\\ d p \;=\; \\\\int^{-}_{p} \\\\ f(p) \\\\ d p$$$
Lean4
theorem lintegral_comp_pi_polarCoord_symm (f : (ι → ℝ × ℝ) → ℝ≥0∞) :
∫⁻ p in (Set.univ.pi fun _ : ι ↦ polarCoord.target), (∏ i, .ofReal (p i).1) * f (fun i ↦ polarCoord.symm (p i)) =
∫⁻ p, f p :=
by
rw [← setLIntegral_univ f, ← setLIntegral_congr pi_polarCoord_symm_target_ae_eq_univ]
convert
(lintegral_image_eq_lintegral_abs_det_fderiv_mul volume measurableSet_pi_polarCoord_target
(fun p _ ↦ (hasFDerivAt_pi_polarCoord_symm p).hasFDerivWithinAt) injOn_pi_polarCoord_symm f).symm using
1
refine setLIntegral_congr_fun measurableSet_pi_polarCoord_target (fun x hx ↦ ?_)
simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦ abs_nonneg _),
abs_fst_of_mem_pi_polarCoord_target hx]
