English
The integral identity holds for integrating over the real mixed space after applying polarCoordReal.symm.
Русский
Интегральная тождество для интегрирования после применения polarCoordReal.symm.
LaTeX
$$$\\int x in (realMixedSpace(K)).target \\; f(x) = \\int x, f(x)$$$
Lean4
theorem lintegral_comp_polarCoordReal_symm (f : realMixedSpace K → ℝ≥0∞) :
∫⁻ x in (polarCoordReal K).target, (∏ w : { w // IsComplex w }, .ofReal (x.2 w).1) * f ((polarCoordReal K).symm x) =
∫⁻ x, f x :=
by
rw [← setLIntegral_univ f, ← setLIntegral_congr (polarCoordReal_symm_target_ae_eq_univ K),
lintegral_image_eq_lintegral_abs_det_fderiv_mul volume (polarCoordReal K).open_target.measurableSet
(fun x _ ↦ (hasFDerivAt_polarCoordReal_symm K x).hasFDerivWithinAt) (polarCoordReal K).symm.injOn f]
refine setLIntegral_congr_fun (polarCoordReal K).open_target.measurableSet (fun x hx ↦ ?_)
simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦ abs_nonneg _),
abs_of_mem_polarCoordReal_target K hx]
