English
The a.e. equality of the image of the universal pi-polarCoord_symm map with Set.univ holds with respect to measure volume.
Русский
Справедливо a.e. равенство образа отображения polarCoord.symm в произведении множеств и Set.univ по мере объема.
LaTeX
$$$(\mathrm{Pi.map}(\lambda _\! : ι \mapsto polarCoord.symm) '' \mathrm{Set.univ.pi} \; \mathrm{polarCoord.target}) =^\mathrm{a.e.}_{\mathrm{volume}} \mathrm{Set.univ}.$$$
Lean4
theorem integral_comp_pi_polarCoord_symm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (ι → ℝ × ℝ) → E) :
(∫ p in (Set.univ.pi fun _ : ι ↦ polarCoord.target), (∏ i, (p i).1) • f (fun i ↦ polarCoord.symm (p i))) =
∫ p, f p :=
by
rw [← setIntegral_univ (f := f), ← setIntegral_congr_set pi_polarCoord_symm_target_ae_eq_univ]
convert
(integral_image_eq_integral_abs_det_fderiv_smul volume measurableSet_pi_polarCoord_target
(fun p _ ↦ (hasFDerivAt_pi_polarCoord_symm p).hasFDerivWithinAt) injOn_pi_polarCoord_symm f).symm using
1
refine setIntegral_congr_fun measurableSet_pi_polarCoord_target fun x hx ↦ ?_
simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, abs_fst_of_mem_pi_polarCoord_target hx]
