English
An integral identity expresses that integrating after applying polarCoord inverse is the same as integrating the function itself over the original space.
Русский
Интеграл после применения обратной полярной координаты равен интегралу по исходному пространству.
LaTeX
$$$\\int_{(\\mathrm{polarCoord}(K)).\\mathrm{target}} \\Big(\\prod_{w:\\{ w\\mid IsComplex w\\}} (x.2 w).1\\Big) \\cdot f((\\mathrm{polarCoord}(K)).\\mathrm{symm}x) \\, dx = \\int_{x} f(x) \\, dx$$
Lean4
protected theorem integral_comp_polarCoord_symm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
(f : mixedSpace K → E) :
∫ x in (mixedEmbedding.polarCoord K).target,
(∏ w : { w // IsComplex w }, (x.2 w).1) • f ((mixedEmbedding.polarCoord K).symm x) =
∫ x, f x :=
by
rw [←
(volume_preserving_mixedSpaceToRealMixedSpace_symm K).integral_comp
(mixedSpaceToRealMixedSpace K).symm.measurableEmbedding,
← integral_comp_polarCoordReal_symm, polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq,
Function.comp_def]
