English
Equivalently, the target of polarSpaceCoord is a product of coordinate-wise intervals determined by real vs complex places.
Русский
Аналогично, целевое множество polarSpaceCoord является произведением по координатам интервальных множеств, зависящих от реальных и комплексных мест.
LaTeX
$$$ (polarSpaceCoord(K)).target = (Set.univ.pi \\{w\\;\\mid\\; w.IsReal\\}) \\timesˢ (Set.univ.pi (\\lambda \\_ : \\text{something}) ) $$$
Lean4
theorem integral_comp_polarSpaceCoord_symm [NumberField K] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
(f : mixedSpace K → E) :
∫ x in (polarSpaceCoord K).target, (∏ w : { w // IsComplex w }, x.1 w.1) • f ((polarSpaceCoord K).symm x) =
∫ x, f x :=
by
rw [←
(volume_preserving_homeoRealMixedSpacePolarSpace K).setIntegral_preimage_emb
(homeoRealMixedSpacePolarSpace K).measurableEmbedding,
← mixedEmbedding.integral_comp_polarCoord_symm, polarSpaceCoord_target, ← Homeomorph.image_eq_preimage,
Homeomorph.preimage_image, mixedEmbedding.polarCoord_target]
simp_rw [polarSpaceCoord_symm_apply, mixedEmbedding.polarCoord_symm_apply,
homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal, homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex,
homeoRealMixedSpacePolarSpace_apply_snd]
