English
The symmetric polarCoordReal mapping is compatible with the inverse of the mixed embedding real-space map.
Русский
Обратная полярная координата совместима с обратной картой смешанного вложения в реальном пространстве.
LaTeX
$$$\\text{polarCoordReal_symm_apply}(K):\\; \\text{(polarCoordReal(K)).symm}(x) = \\dots$$$
Lean4
theorem integral_comp_polarCoordReal_symm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
(f : realMixedSpace K → E) :
∫ x in (polarCoordReal K).target, (∏ w : { w // IsComplex w }, (x.2 w).1) • f ((polarCoordReal K).symm x) =
∫ x, f x :=
by
rw [← setIntegral_univ (f := f), ← setIntegral_congr_set (polarCoordReal_symm_target_ae_eq_univ K),
integral_image_eq_integral_abs_det_fderiv_smul volume (polarCoordReal K).open_target.measurableSet
(fun x _ ↦ (hasFDerivAt_polarCoordReal_symm K x).hasFDerivWithinAt) (polarCoordReal K).symm.injOn f]
refine setIntegral_congr_fun (polarCoordReal K).open_target.measurableSet fun x hx ↦ ?_
simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod, abs_of_mem_polarCoordReal_target K hx]
