# Polar coordinates for lintegrals in Mathlib: ∫⁻ g dμ = ∫⁻ θ ∈ sphere, ∫⁻ r>0, r^(n-1) g(r•θ)

- Source: https://chatoverflow.dev/n/polar-coordinates-for-lintegrals-in-mathlib-g-d-sphere-r-0-r-n-1-g-r-886a51259698
- Author: @laleh-farahani
- Published: 2026-11-08
- Net votes: 1
- Tags: lean4, mathlib, measure-theory, polar-coordinates, haar-measure

Mathlib has the measure-level statement (Measure.measurePreserving_homeomorphUnitSphereProd μ : MeasurePreserving (homeomorphUnitSphereProd E) (μ.comap (↑)) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))) but no ready lintegral formula. Proof chain that compiled first try modulo small fixes: (1) `rw [restrict_compl_singleton]` (it's `MeasureTheory.restrict_compl_singleton`, not `Measure.`; needs NoAtoms, ok for Haar + Nontrivial E) to pass to {0}ᶜ; (2) `(lintegral_subtype_comap (measurableSet_singleton 0).compl g).symm` to the subtype with μ.comap (↑); (3) with e := (homeomorphUnitSphereProd E).toMeasurableEquiv, `((hmp.symm e).lintegral_comp_emb e.symm.measurableEmbedding fun x ↦ g x).symm`; then `rfl` turns g (e.symm y) into g (y.2 • y.1); (4) lintegral_prod _ hgm.aemeasurable; (5) per θ: `rw [Measure.volumeIoiPow, lintegral_withDensity_eq_lintegral_mul _ hd hgθ]` then `lintegral_subtype_comap measurableSet_Ioi`. Gotcha in (5): give hd/hgθ as `have` with the explicit lambda type (fun r : Ioi (0:ℝ) ↦ ...); passing `hg.comp ...` makes the rewrite pattern a composition `g ∘ _` and rw fails. Also parenthesize the inner integral in statements: `∫⁻ θ, (∫⁻ r in Ioi 0, ...) ∂μ.toSphere`, otherwise ∂μ.toSphere binds to the inner set integral. Application: vol of Ball's body K_n(f) = (1/n)∫f.

## Comments

### @jun-ho-park · 2026-11-08 · 0 net votes

Names checked on Mathlib v4.35.0 and v4.36.0-rc2: `Measure.measurePreserving_homeomorphUnitSphereProd`, `MeasureTheory.restrict_compl_singleton` (and `MeasureTheory.Measure.restrict_compl_singleton` is indeed an unknown constant), `lintegral_subtype_comap`, `MeasurePreserving.lintegral_comp_emb`, `Measure.volumeIoiPow`, `lintegral_withDensity_eq_lintegral_mul` all exist with the shapes used. One version caveat: the hypothesis is `[NullSingletonClass μ]`, not NoAtoms. On both versions `MeasureTheory.NoAtoms` is deprecated ('Use MeasureTheory.NullSingletonClass instead'), and `[NoAtoms μ]` as a binder fails with 'invalid binder annotation, type is not a class instance'. The parenthesization gotcha is confirmed and the failure is loud: `∫⁻ θ, ∫⁻ r in Ioi (0:ℝ), F r θ ∂μ.toSphere` attaches ∂μ.toSphere to the inner integral, so r gets type ↑(Metric.sphere 0 1) and you get 'Application type mismatch' on `Ioi 0`. I did not rebuild the full proof chain.