Integration in polar coordinates

Let E be a nontrivial finite-dimensional real normed space of dimension d 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 ^ (d - 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 ^ (d - 1) • f (r • u) ∂μ.toSphere = ∫ r in (0, ∞), r ^ (d - 1) • ∫ u ∈ S, f (r • u) ∂μ.toSphere,

and uses the first for a radial fundamental theorem of calculus: for a C¹ function f with compact support,

∫ x, ‖x‖ ^ (-d) * f' x x ∂μ = -(d * μ (ball 0 1)) * f 0.

In the language of distributions the second formula says that the vector field x / ‖x‖ ^ d has divergence d μ(ball 0 1) δ₀; it is the flux computation behind the fundamental solution of the Laplacian.

Main declarations

• TauCeti.integral_volumeIoiPow: integration against Mathlib's radial measure MeasureTheory.Measure.volumeIoiPow k is integration on (0, ∞) against the weight r ^ k.
• TauCeti.integral_eq_integral_toSphere_integral_Ioi: integration in polar coordinates, with the sphere variable outermost.
• TauCeti.integral_eq_integral_Ioi_integral_toSphere: integration in polar coordinates, with the radial variable outermost.
• TauCeti.integral_norm_rpow_neg_finrank_mul_fderiv_apply_self: the radial fundamental theorem of calculus.
• ContinuousOn.integral_toSphere_smul: the sphere integrals r ↦ ∫ u ∈ S, f (r • u) depend continuously on the radius r ∈ [0, R] when f is continuous on the closed ball of radius R.
• TauCeti.setIntegral_ball_zero_eq_integral_Ioo, TauCeti.integral_Ioo_pow_mul_toSphere_real_univ: integration over a ball about the origin in polar coordinates, and the corresponding formula for the measure of the ball.

theorem TauCeti.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 TauCeti.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 TauCeti.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 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.

theorem TauCeti.setIntegral_ball_zero_eq_integral_Ioo {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} {R : ℝ} (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R) μ) : ∫ (x : E) in Metric.ball 0 R, f x ∂μ = ∫ (s : ℝ) in Set.Ioo 0 R, s ^ (Module.finrank ℝ E - 1) • ∫ (θ : ↑(Metric.sphere 0 1)), f (s • ↑θ) ∂μ.toSphere

Integration over a ball in polar coordinates. For f integrable on the ball ball 0 R, the integral of f over ball 0 R is the integral over the radii s ∈ (0, R) of the sphere integrals, against the radial Jacobian s ^ (d - 1).

theorem TauCeti.integral_Ioo_pow_mul_toSphere_real_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {R : ℝ} : (∫ (s : ℝ) in Set.Ioo 0 R, s ^ (Module.finrank ℝ E - 1)) * μ.toSphere.real Set.univ = μ.real (Metric.ball 0 R)

The radial Jacobian integrates against the total surface measure to the measure of the ball: (∫ s in (0, R), s ^ (d - 1)) * μ.toSphere(S) = μ (ball 0 R).

theorem TauCeti.integral_norm_rpow_neg_finrank_mul_fderiv_apply_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {f : E → ℝ} (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f) : ∫ (x : E), ‖x‖ ^ (-↑(Module.finrank ℝ E)) * (fderiv ℝ f x) x ∂μ = -(↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1)) * f 0

Radial fundamental theorem of calculus. For a C¹ function f with compact support on a nontrivial finite-dimensional real normed space of dimension d, ∫ ‖x‖ ^ (-d) * f' x x ∂μ = -(d * μ (ball 0 1)) * f 0.

In the language of distributions, div (x / ‖x‖ ^ d) = d μ(ball 0 1) δ₀.