English
There is a corresponding lintegral identity for polarSpaceCoord_symm with ENNReal-valued functions.
Русский
Существует соответствующее линегральное тождество для polarSpaceCoord_symm с функциями ENNReal.
LaTeX
$$$\\mathrm{lintegral}\\; f = \\mathrm{lintegral}\\; f\\circ (polarSpaceCoord(K)).\\mathrm{symm}$$$
Lean4
theorem lintegral_comp_polarSpaceCoord_symm [NumberField K] (f : mixedSpace K → ℝ≥0∞) :
∫⁻ x in (polarSpaceCoord K).target,
(∏ w : { w // IsComplex w }, .ofReal (x.1 w.1)) * f ((polarSpaceCoord K).symm x) =
∫⁻ x, f x :=
by
rw [←
(volume_preserving_homeoRealMixedSpacePolarSpace K).setLIntegral_comp_preimage_emb
(homeoRealMixedSpacePolarSpace K).measurableEmbedding,
← mixedEmbedding.lintegral_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]
