Integration in polar coordinates (ported from TauCeti)

Let E be a nontrivial finite-dimensional real normed space of dimension n with an additive Haar measure μ. Mathlib's MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd identifies μ on E \ {0} with the product of the surface measure μ.toSphere on the unit sphere and the radial measure r ^ (n - 1) dr on (0, ∞), but upstream only integrates radial functions against it (MeasureTheory.integral_fun_norm_addHaar). This file records the integral formula for an arbitrary integrable function, in both orders of integration,

∫ x, f x ∂μ = ∫ u ∈ S, ∫ r in (0, ∞), r ^ (n - 1) • f (r • u) ∂μ.toSphere = ∫ r in (0, ∞), r ^ (n - 1) • ∫ u ∈ S, f (r • u) ∂μ.toSphere.

Main declarations

• integral_volumeIoiPow: integration against Measure.volumeIoiPow k is integration on (0, ∞) against the weight r ^ k.
• integral_eq_integral_toSphere_integral_Ioi, integral_eq_integral_Ioi_integral_toSphere: integration in polar coordinates.
• continuousOn_integral_toSphere_smul: the sphere integrals r ↦ ∫ u ∈ S, f (r • u) depend continuously on r ∈ [0, R] when f is continuous on the closed ball of radius R.

Provenance

Pool port: imports relocated under LeanPool.ViscositySolutionTheory; original mathematical namespaces and copyright retained; checked with Lean/Mathlib v4.34.0.

• Upstream: TauCeti, https://github.com/TauCetiProject/TauCeti
• Path: TauCeti/MeasureTheory/Constructions/HaarToSphere.lean
• Commit: 91f66a0514e6523efdccddb9e35fb82c96dd6405 (2026-09-24)
• License: Apache-2.0. Upstream NOTICE: none.
• Upstream notice: Copyright (c) 2026 The Tau Ceti contributors. All rights reserved.; upstream authors: The Tau Ceti contributors.
• Extent: integral_volumeIoiPow, integrable_and_integral_eq_integral_prod_toSphere, integral_eq_integral_toSphere_integral_Ioi, integral_eq_integral_Ioi_integral_toSphere, ContinuousOn.integral_toSphere_smul (verbatim up to naming).
• Changes: ported from Lean v4.34.0-rc2 to Lean/Mathlib v4.30.0; module/public import removed; namespace TauCeti → ViscositySolns.Analysis; ContinuousOn.integral_toSphere_smul renamed continuousOn_integral_toSphere_smul; the radial fundamental theorem of calculus (integral_norm_rpow_neg_finrank_mul_fderiv_apply_self) is not ported.

theorem ViscositySolns.Analysis.integral_volumeIoiPow {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ) (h : ℝ → F) : ∫ (r : ↑(Set.Ioi 0)), h ↑r ∂MeasureTheory.Measure.volumeIoiPow k = ∫ (r : ℝ) in Set.Ioi 0, r ^ k • h r

Integration against MeasureTheory.Measure.volumeIoiPow k is integration on (0, ∞) against the weight r ^ k.

theorem ViscositySolns.Analysis.integral_eq_integral_toSphere_integral_Ioi {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (hf : MeasureTheory.Integrable f μ) : ∫ (x : E), f x ∂μ = ∫ (u : ↑(Metric.sphere 0 1)), ∫ (r : ℝ) in Set.Ioi 0, r ^ (Module.finrank ℝ E - 1) • f (r • ↑u) ∂μ.toSphere

Integration in polar coordinates. An integrable function on a finite-dimensional real normed space is integrated by first integrating along each ray r ↦ r • u, against the radial Jacobian r ^ (d - 1), and then over the unit sphere against μ.toSphere.

theorem ViscositySolns.Analysis.integral_eq_integral_Ioi_integral_toSphere {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (hf : MeasureTheory.Integrable f μ) : ∫ (x : E), f x ∂μ = ∫ (r : ℝ) in Set.Ioi 0, r ^ (Module.finrank ℝ E - 1) • ∫ (u : ↑(Metric.sphere 0 1)), f (r • ↑u) ∂μ.toSphere

Integration in polar coordinates, radial variable outermost. An integrable function on a finite-dimensional real normed space is integrated by first integrating over the sphere of radius r (parametrized by the unit sphere against μ.toSphere), and then in r against the radial Jacobian r ^ (d - 1).

theorem ViscositySolns.Analysis.continuousOn_integral_toSphere_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {R : ℝ} (hf : ContinuousOn f (Metric.closedBall 0 R)) : ContinuousOn (fun (r : ℝ) => ∫ (u : ↑(Metric.sphere 0 1)), f (r • ↑u) ∂μ.toSphere) (Set.Icc 0 R)

The integral of f over the sphere of radius r about the origin, parametrized by the unit sphere, depends continuously on r ∈ [0, R] when f is continuous on the closed ball of radius R.