English
The integral over the polar target with the product of the first-components equals the integral over the whole domain for vector-valued f.
Русский
Интеграл по полярной цели с произведением первых координат равен интегралу по всей области для векторно-значной функции f.
LaTeX
$$$\int_{p \in (\mathrm{Set.univ.pi}\; \mathrm{polarCoord.target})} \Big( \prod_i (p_i)_1 \Big) \cdot f(\mathrm{polarCoord.symm}(p)) \, dp = \int_p f(p) \, dp.$$$
Lean4
protected theorem lintegral_comp_pi_polarCoord_symm (f : (ι → ℂ) → ℝ≥0∞) :
∫⁻ p in (Set.univ.pi fun _ : ι ↦ Complex.polarCoord.target),
(∏ i, .ofReal (p i).1) * f (fun i ↦ Complex.polarCoord.symm (p i)) =
∫⁻ p, f p :=
by
let e := MeasurableEquiv.piCongrRight (fun _ : ι ↦ measurableEquivRealProd.symm)
have := volume_preserving_pi (fun _ : ι ↦ Complex.volume_preserving_equiv_real_prod.symm)
rw [← MeasurePreserving.lintegral_comp_emb this e.measurableEmbedding]
exact lintegral_comp_pi_polarCoord_symm (f ∘ e)
