Hausdorff measure of spheres

Let E be a real inner product space of dimension n. Mathlib's surface measure Measure.toSphere volume on the unit sphere is defined through cones: a set s of the sphere has measure n times the volume of Ioo 0 1 • s. This file identifies it with the normalized (n - 1)-dimensional Hausdorff measure μHE[n - 1] of the sphere, and deduces

μHE[n - 1] (sphere c r) = n ω_n r ^ (n - 1), for r > 0,

where ω_n = volume (ball 0 1). These are the constants of polar integration with respect to Hausdorff measure, and they agree with Mathlib's volume of balls. The passage from the unit sphere to sphere c r is a rescaling statement valid for every dimension d in every real normed space: μHE[d] on sphere c r is r ^ d times the pushforward of μHE[d] on the unit sphere by u ↦ c + r • u.

The comparison is a cone formula for parametrizations of pieces of the unit sphere. If ψ : W → E takes values in the unit sphere near a measurable set s, where dim W = n - 1, and ψ is injective on s with injective derivative, then (t, w) ↦ t • ψ w parametrizes the cone Ioo 0 1 • ψ '' s. Since ψ w is a unit vector orthogonal to the range of the derivative of ψ, the Jacobian of the cone map at (t, w) is t ^ (n - 1) times the Jacobian of ψ at w (LinearMap.normDet_toSpanSingleton_coprod). The area formula applied to both maps, and integration of t ^ (n - 1) over (0, 1), give μHE[n - 1] (ψ '' s) = n volume (Ioo 0 1 • ψ '' s). The inverse of Mathlib's stereographic projection from a unit vector v parametrizes the sphere minus v in this way, and the projections from v and -v together cover the sphere. No lower bound on the dimension is needed: in dimension one, both measures count points.

Main results

• TauCeti.euclideanHausdorffMeasure_restrict_sphere_eq_smul_map: rescaling Hausdorff measure on spheres, with the integral and integrability forms TauCeti.setLIntegral_sphere_eq_mul_setLIntegral_sphere_zero_one, TauCeti.setIntegral_sphere_eq_smul_setIntegral_sphere_zero_one and TauCeti.integrableOn_sphere_iff.
• TauCeti.euclideanHausdorffMeasure_image_eq_finrank_mul_volume_Ioo_smul: the cone formula for a regular injective parametrization of a piece of the unit sphere.
• TauCeti.toSphere_volume_eq_comap_euclideanHausdorffMeasure: Mathlib's surface measure on the unit sphere is normalized (n - 1)-dimensional Hausdorff measure.
• TauCeti.euclideanHausdorffMeasure_restrict_sphere: the same comparison as measures on E.
• TauCeti.euclideanHausdorffMeasure_sphere_zero_one_eq_ofReal: the unit sphere has (n - 1)-dimensional Hausdorff measure 2 π ^ (n / 2) / Γ(n / 2).
• TauCeti.toSphere_volume_apply_univ: the same value 2 π ^ (n / 2) / Γ(n / 2) for the total mass of Mathlib's surface measure Measure.toSphere volume.
• TauCeti.euclideanHausdorffMeasure_sphere: μHE[n - 1] (sphere c r) = n ω_n r ^ (n - 1).
• TauCeti.roundSphereVolume: the area |Sⁿ| of the unit round sphere Sⁿ ⊆ ℝⁿ⁺¹, its normalized n-dimensional Hausdorff measure (not the ambient Lebesgue measure, which vanishes).
• TauCeti.euclideanHausdorffMeasure_sphere_eq_ofReal_roundSphereVolume: the unit sphere of every real inner product space of dimension n + 1 has n-dimensional Hausdorff measure |Sⁿ|; in particular this measure is finite.
• TauCeti.roundSphereVolume_eq_two_mul_pi_rpow_div_Gamma, TauCeti.roundSphereVolume_pos: the value |Sⁿ| = 2 π ^ ((n + 1) / 2) / Γ((n + 1) / 2) and the positivity of |Sⁿ|.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §3.3 (the area formula).

theorem TauCeti.euclideanHausdorffMeasure_restrict_sphere_eq_smul_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (d : ℕ) (c : E) {r : ℝ} (hr : 0 < r) : (MeasureTheory.Measure.euclideanHausdorffMeasure d).restrict (Metric.sphere c r) = ENNReal.ofReal r ^ d • MeasureTheory.Measure.map (fun (u : E) => c + r • u) ((MeasureTheory.Measure.euclideanHausdorffMeasure d).restrict (Metric.sphere 0 1))

Rescaling Hausdorff measure on spheres. For r > 0, the d-dimensional Hausdorff measure on the sphere sphere c r is r ^ d times the pushforward of the d-dimensional Hausdorff measure on the unit sphere by u ↦ c + r • u.

theorem TauCeti.setLIntegral_sphere_eq_mul_setLIntegral_sphere_zero_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (d : ℕ) (c : E) {r : ℝ} (hr : 0 < r) (f : E → ENNReal) : ∫⁻ (y : E) in Metric.sphere c r, f y ∂MeasureTheory.Measure.euclideanHausdorffMeasure d = ENNReal.ofReal r ^ d * ∫⁻ (u : E) in Metric.sphere 0 1, f (c + r • u) ∂MeasureTheory.Measure.euclideanHausdorffMeasure d

Rescaling integrals over spheres. For r > 0, integrating a nonnegative function against d-dimensional Hausdorff measure on sphere c r amounts to integrating its pullback by u ↦ c + r • u over the unit sphere, with the factor r ^ d.

theorem TauCeti.setIntegral_sphere_eq_smul_setIntegral_sphere_zero_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (d : ℕ) (c : E) {r : ℝ} (hr : 0 < r) (f : E → F) : ∫ (y : E) in Metric.sphere c r, f y ∂MeasureTheory.Measure.euclideanHausdorffMeasure d = r ^ d • ∫ (u : E) in Metric.sphere 0 1, f (c + r • u) ∂MeasureTheory.Measure.euclideanHausdorffMeasure d

Rescaling integrals over spheres. For r > 0, integrating a function against d-dimensional Hausdorff measure on sphere c r amounts to integrating its pullback by u ↦ c + r • u over the unit sphere, with the factor r ^ d.

theorem TauCeti.integrableOn_sphere_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [TopologicalSpace F] [ESeminormedAddMonoid F] (d : ℕ) (c : E) {r : ℝ} (hr : 0 < r) {f : E → F} : MeasureTheory.IntegrableOn f (Metric.sphere c r) (MeasureTheory.Measure.euclideanHausdorffMeasure d) ↔ MeasureTheory.IntegrableOn (fun (u : E) => f (c + r • u)) (Metric.sphere 0 1) (MeasureTheory.Measure.euclideanHausdorffMeasure d)

A function is integrable for d-dimensional Hausdorff measure on sphere c r, r > 0, if and only if its pullback by u ↦ c + r • u is integrable on the unit sphere.

theorem TauCeti.euclideanHausdorffMeasure_image_eq_finrank_mul_volume_Ioo_smul {W : Type u_1} {E : Type u_2} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ψ : W → E} {s : Set W} (hdim : Module.finrank ℝ W + 1 = Module.finrank ℝ E) (hs : MeasurableSet s) (hψ : ∀ w ∈ s, ∀ᶠ (y : W) in nhds w, ‖ψ y‖ = 1) (hd : ∀ w ∈ s, DifferentiableAt ℝ ψ w) (hinj : ∀ w ∈ s, Function.Injective ⇑(fderiv ℝ ψ w)) (hψs : Set.InjOn ψ s) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ W)) (ψ '' s) = ↑(Module.finrank ℝ E) * MeasureTheory.volume (Set.Ioo 0 1 • ψ '' s)

Cone formula. Let ψ : W → E take values in the unit sphere near a measurable set s, where dim W + 1 = dim E, and let ψ be injective on s and differentiable on s with injective derivative. Then the dim W-dimensional Hausdorff measure of ψ '' s is dim E times the volume of the cone Ioo 0 1 • ψ '' s.

theorem TauCeti.toSphere_volume_eq_comap_euclideanHausdorffMeasure {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : MeasureTheory.volume.toSphere = MeasureTheory.Measure.comap Subtype.val (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E - 1))

Mathlib's surface measure Measure.toSphere volume on the unit sphere of an n-dimensional real inner product space is normalized (n - 1)-dimensional Hausdorff measure.

theorem TauCeti.euclideanHausdorffMeasure_restrict_sphere {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E - 1)).restrict (Metric.sphere 0 1) = MeasureTheory.Measure.map Subtype.val MeasureTheory.volume.toSphere

Normalized (n - 1)-dimensional Hausdorff measure restricted to the unit sphere of an n-dimensional real inner product space is the pushforward of Mathlib's surface measure Measure.toSphere volume.

theorem TauCeti.euclideanHausdorffMeasure_sphere_zero_one {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E - 1)) (Metric.sphere 0 1) = ↑(Module.finrank ℝ E) * MeasureTheory.volume (Metric.ball 0 1)

The unit sphere of an n-dimensional real inner product space has (n - 1)-dimensional Hausdorff measure n ω_n, where ω_n is the volume of the unit ball.

theorem TauCeti.euclideanHausdorffMeasure_sphere_zero_one_eq_ofReal {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E - 1)) (Metric.sphere 0 1) = ENNReal.ofReal (2 * Real.pi ^ (↑(Module.finrank ℝ E) / 2) / Real.Gamma (↑(Module.finrank ℝ E) / 2))

The unit sphere of an n-dimensional real inner product space has (n - 1)-dimensional Hausdorff measure 2 π ^ (n / 2) / Γ(n / 2). In dimension zero both sides vanish.

theorem TauCeti.toSphere_volume_apply_univ {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : MeasureTheory.volume.toSphere Set.univ = ENNReal.ofReal (2 * Real.pi ^ (↑(Module.finrank ℝ E) / 2) / Real.Gamma (↑(Module.finrank ℝ E) / 2))

The surface area of the unit sphere. On a real inner product space of dimension n, Mathlib's surface measure Measure.toSphere volume gives the unit sphere total mass 2 π ^ (n / 2) / Γ(n / 2). In dimension zero the sphere is empty and both sides vanish.

theorem TauCeti.euclideanHausdorffMeasure_sphere {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (c : E) {r : ℝ} (hr : 0 < r) : (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E - 1)) (Metric.sphere c r) = ↑(Module.finrank ℝ E) * MeasureTheory.volume (Metric.ball 0 1) * ENNReal.ofReal r ^ (Module.finrank ℝ E - 1)

A sphere of radius r > 0 in an n-dimensional real inner product space has (n - 1)-dimensional Hausdorff measure n ω_n r ^ (n - 1), where ω_n is the volume of the unit ball.

noncomputable def TauCeti.roundSphereVolume (n : ℕ) : ℝ

The area |Sⁿ| of the unit round sphere Sⁿ ⊆ ℝⁿ⁺¹: the normalized n-dimensional Hausdorff measure of the unit sphere of EuclideanSpace ℝ (Fin (n + 1)).

theorem TauCeti.roundSphereVolume_def (n : ℕ) : roundSphereVolume n = ((MeasureTheory.Measure.euclideanHausdorffMeasure n) (Metric.sphere 0 1)).toReal

Unfolding lemma for TauCeti.roundSphereVolume.

theorem TauCeti.roundSphereVolume_eq_two_mul_pi_rpow_div_Gamma (n : ℕ) : roundSphereVolume n = 2 * Real.pi ^ ((↑n + 1) / 2) / Real.Gamma ((↑n + 1) / 2)

The area of the unit round sphere: |Sⁿ| = 2 π ^ ((n + 1) / 2) / Γ((n + 1) / 2).

theorem TauCeti.roundSphereVolume_pos (n : ℕ) : 0 < roundSphereVolume n

The unit round sphere has positive area.

theorem TauCeti.euclideanHausdorffMeasure_sphere_eq_ofReal_roundSphereVolume {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {n : ℕ} (hE : Module.finrank ℝ E = n + 1) : (MeasureTheory.Measure.euclideanHausdorffMeasure n) (Metric.sphere 0 1) = ENNReal.ofReal (roundSphereVolume n)

The unit sphere of every real inner product space of dimension n + 1 has normalized n-dimensional Hausdorff measure |Sⁿ|. In particular, this measure is finite.