English
For a function f: (ι → ℂ) → E, the polar-coordinate transformation preserves the integral: the integral over the π-product space with the product of first coordinates equals the integral of f over the whole space.
Русский
Для функции f: (ι → ℂ) → E интеграл сохраняется при переходе по полярным координатам: интеграл по произведению π пространства с произведением действительных частей равно интегралу по всему пространству.
LaTeX
$$$$\int_{p \in (\mathrm{Set.univ}.\pi\ { _ : ι \mapsto \mathbb{C}.\text{polarCoord}.target})} \Big(\prod_i (p_i)_1\Big) \cdot f\bigl(\lambda i, \mathrm{polarCoord}.symm(p_i)\bigr) \, dp = \int_p f(p) \, dp.$$$$
Lean4
protected theorem integral_comp_pi_polarCoord_symm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
(f : (ι → ℂ) → E) :
(∫ p in (Set.univ.pi fun _ : ι ↦ Complex.polarCoord.target),
(∏ i, (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.integral_comp this e.measurableEmbedding f]
exact integral_comp_pi_polarCoord_symm (f ∘ e)
