diff --git a/PhysLean.lean b/PhysLean.lean
index 920ac6ec..5826b403 100644
--- a/PhysLean.lean
+++ b/PhysLean.lean
@@ -344,10 +344,11 @@ import PhysLean.SpaceAndTime.Space.Derivatives.Grad
 import PhysLean.SpaceAndTime.Space.Derivatives.Laplacian
 import PhysLean.SpaceAndTime.Space.DistConst
 import PhysLean.SpaceAndTime.Space.DistOfFunction
+import PhysLean.SpaceAndTime.Space.Integrals.Basic
+import PhysLean.SpaceAndTime.Space.Integrals.RadialAngularMeasure
 import PhysLean.SpaceAndTime.Space.IsDistBounded
 import PhysLean.SpaceAndTime.Space.LengthUnit
 import PhysLean.SpaceAndTime.Space.Norm
-import PhysLean.SpaceAndTime.Space.RadialAngularMeasure
 import PhysLean.SpaceAndTime.Space.Slice
 import PhysLean.SpaceAndTime.Space.Translations
 import PhysLean.SpaceAndTime.SpaceTime.Basic
diff --git a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
index 85f8105e..301024f2 100644
--- a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
+++ b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
@@ -287,17 +287,12 @@ lemma threeDimPointParticle_div_electricField {𝓕} (q : ℝ) (r₀ : Space 3)
     simp [distTranslate_ofFunction]
   simp only [Int.reduceNeg, zpow_neg, one_div]
   rw [constantTime_distSpaceDiv, distDiv_distTranslate, h1]
-  simp only [map_smul]
-  suffices h : volume.real (Metric.ball (0 : Space 3) 1) = (4/3 * Real.pi) by
-    rw [h]
-    simp [smul_smul]
-    ext η
-    simp [constantTime_apply, diracDelta_apply, distTranslate_apply]
-    left
-    ring_nf
-    field_simp
-  simp [MeasureTheory.Measure.real]
-  exact pi_nonneg
+  simp only [map_smul, smul_smul]
+  ext η
+  simp [constantTime_apply, diracDelta_apply, distTranslate_apply]
+  left
+  ring_nf
+  field_simp
 
 lemma threeDimPointParticle_isExterma (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) :
     (threeDimPointParticle 𝓕 q r₀).IsExtrema 𝓕 (threeDimPointParticleCurrentDensity 𝓕.c q r₀) := by
diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index 097d6618..c7d3c4b6 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -712,9 +712,6 @@ lemma oneEquiv_measurePreserving : MeasurePreserving oneEquiv volume volume :=
 lemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume volume := by
   exact LinearIsometryEquiv.measurePreserving oneEquiv.symm
 
-lemma volume_eq_addHaar {d} : (volume (α := Space d)) = Space.basis.toBasis.addHaar := by
-  exact (OrthonormalBasis.addHaar_eq_volume _).symm
-
 instance {d : ℕ} : Nontrivial (Space d.succ) := by
   refine { exists_pair_ne := ?_ }
   use 0, basis 0
@@ -729,66 +726,4 @@ instance : Subsingleton (Space 0) := by
   intro x y
   ext i
   fin_cases i
-
-lemma volume_closedBall_ne_zero {d : ℕ} (x : Space d.succ) (r : ℝ) (hr : 0 < r) :
-    volume (Metric.closedBall x r) ≠ 0 := by
-  obtain ⟨k,hk⟩ := Nat.even_or_odd' d.succ
-  rcases hk with hk | hk
-  · rw [InnerProductSpace.volume_closedBall_of_dim_even (k := k)]
-    simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq, mul_eq_zero, Nat.add_eq_zero_iff,
-      one_ne_zero, and_false, not_false_eq_true, pow_eq_zero_iff, ENNReal.ofReal_eq_zero, not_or,
-      not_le]
-    apply And.intro
-    · simp_all
-    · positivity
-    · simpa using hk
-  · rw [InnerProductSpace.volume_closedBall_of_dim_odd (k := k)]
-    simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq, mul_eq_zero, Nat.add_eq_zero_iff,
-      one_ne_zero, and_false, not_false_eq_true, pow_eq_zero_iff, ENNReal.ofReal_eq_zero, not_or,
-      not_le]
-    apply And.intro
-    · simp_all
-    · positivity
-    · simpa using hk
-
-lemma volume_closedBall_ne_top {d : ℕ} (x : Space d.succ) (r : ℝ) :
-    volume (Metric.closedBall x r) ≠ ⊤ := by
-  obtain ⟨k,hk⟩ := Nat.even_or_odd' d.succ
-  rcases hk with hk | hk
-  · rw [InnerProductSpace.volume_closedBall_of_dim_even (k := k)]
-    simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq]
-    apply not_eq_of_beq_eq_false
-    rfl
-    simpa using hk
-  · rw [InnerProductSpace.volume_closedBall_of_dim_odd (k := k)]
-    simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq]
-    apply not_eq_of_beq_eq_false
-    rfl
-    simpa using hk
-
-@[simp]
-lemma volume_metricBall_three :
-    volume (Metric.ball (0 : Space 3) 1) = ENNReal.ofReal (4 / 3 * Real.pi) := by
-  rw [InnerProductSpace.volume_ball_of_dim_odd (k := 1)]
-  simp only [ENNReal.ofReal_one, finrank_eq_dim, one_pow, pow_one, Nat.reduceAdd,
-    Nat.doubleFactorial.eq_3, Nat.doubleFactorial, mul_one, Nat.cast_ofNat, one_mul]
-  ring_nf
-  simp
-
-@[simp]
-lemma volume_metricBall_two :
-    volume (Metric.ball (0 : Space 2) 1) = ENNReal.ofReal Real.pi := by
-  rw [InnerProductSpace.volume_ball_of_dim_even (k := 1)]
-  simp [finrank_eq_dim]
-  simp [finrank_eq_dim]
-
-@[simp]
-lemma volume_metricBall_two_real :
-    (volume.real (Metric.ball (0 : Space 2) 1)) = Real.pi := by
-  trans (volume (Metric.ball (0 : Space 2) 1)).toReal
-  · rfl
-  rw [volume_metricBall_two]
-  simp only [ENNReal.toReal_ofReal_eq_iff]
-  exact Real.pi_nonneg
-
 end Space
diff --git a/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
new file mode 100644
index 00000000..e05b988e
--- /dev/null
+++ b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
@@ -0,0 +1,231 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import PhysLean.SpaceAndTime.Space.Basic
+/-!
+
+# Integrals in Space
+
+## i. Overview
+
+In this module we give general properties of integrals over `Space d`.
+We focus here on the volume measure, which is the usual measure on `Space d`, i.e.
+`dx dy dz`.
+
+## ii. Key results
+
+- `volume_eq_addHaar` : The volume measure on `Space d` is the same as the Haar measure
+  associated with the basis of `Space d`.
+- `integral_volume_eq_spherical` : The integral of a function over `Space d.succ` with
+  respect to the volume measure can be expressed as an integral over the unit sphere and
+  the positive reals.
+- `lintegral_volume_eq_spherical` : The lower Lebesgue integral of a function over `Space d.succ`
+  with respect to the volume measure can be expressed as a lower Lebesgue integral over the unit
+  sphere and the positive reals.
+
+-/
+
+namespace Space
+
+open InnerProductSpace MeasureTheory
+
+/-!
+
+## A. Properties of the volume measure
+
+-/
+
+lemma volume_eq_addHaar {d} : (volume (α := Space d)) = Space.basis.toBasis.addHaar := by
+  exact (OrthonormalBasis.addHaar_eq_volume _).symm
+
+lemma volume_closedBall_ne_zero {d : ℕ} (x : Space d.succ) {r : ℝ} (hr : 0 < r) :
+    volume (Metric.closedBall x r) ≠ 0 := by
+  obtain ⟨k,hk⟩ := Nat.even_or_odd' d.succ
+  rcases hk with hk | hk
+  · rw [InnerProductSpace.volume_closedBall_of_dim_even (k := k)]
+    simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq, mul_eq_zero, Nat.add_eq_zero_iff,
+      one_ne_zero, and_false, not_false_eq_true, pow_eq_zero_iff, ENNReal.ofReal_eq_zero, not_or,
+      not_le]
+    apply And.intro
+    · simp_all
+    · positivity
+    · simpa using hk
+  · rw [InnerProductSpace.volume_closedBall_of_dim_odd (k := k)]
+    simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq, mul_eq_zero, Nat.add_eq_zero_iff,
+      one_ne_zero, and_false, not_false_eq_true, pow_eq_zero_iff, ENNReal.ofReal_eq_zero, not_or,
+      not_le]
+    apply And.intro
+    · simp_all
+    · positivity
+    · simpa using hk
+
+lemma volume_closedBall_ne_top {d : ℕ} (x : Space d.succ) (r : ℝ) :
+    volume (Metric.closedBall x r) ≠ ⊤ := by
+  obtain ⟨k,hk⟩ := Nat.even_or_odd' d.succ
+  rcases hk with hk | hk
+  · rw [InnerProductSpace.volume_closedBall_of_dim_even (by simpa using hk)]
+    simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq]
+    apply not_eq_of_beq_eq_false
+    rfl
+  · rw [InnerProductSpace.volume_closedBall_of_dim_odd (by simpa using hk)]
+    simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq]
+    apply not_eq_of_beq_eq_false
+    rfl
+
+@[simp]
+lemma volume_metricBall_three :
+    volume (Metric.ball (0 : Space 3) 1) = ENNReal.ofReal (4 / 3 * Real.pi) := by
+  rw [InnerProductSpace.volume_ball_of_dim_odd (k := 1)]
+  simp only [ENNReal.ofReal_one, finrank_eq_dim, one_pow, pow_one, Nat.reduceAdd,
+    Nat.doubleFactorial.eq_3, Nat.doubleFactorial, mul_one, Nat.cast_ofNat, one_mul]
+  ring_nf
+  simp
+
+@[simp]
+lemma volume_metricBall_two :
+    volume (Metric.ball (0 : Space 2) 1) = ENNReal.ofReal Real.pi := by
+  rw [InnerProductSpace.volume_ball_of_dim_even (k := 1)]
+  simp [finrank_eq_dim]
+  simp [finrank_eq_dim]
+
+@[simp]
+lemma volume_metricBall_two_real :
+    (volume.real (Metric.ball (0 : Space 2) 1)) = Real.pi := by
+  trans (volume (Metric.ball (0 : Space 2) 1)).toReal
+  · rfl
+  rw [volume_metricBall_two]
+  simp only [ENNReal.toReal_ofReal_eq_iff]
+  exact Real.pi_nonneg
+
+@[simp]
+lemma volume_metricBall_three_real :
+    (volume.real (Metric.ball (0 : Space 3) 1)) = 4 / 3 * Real.pi := by
+  trans (volume (Metric.ball (0 : Space 3) 1)).toReal
+  · rfl
+  rw [volume_metricBall_three]
+  simp only [ENNReal.toReal_ofReal_eq_iff]
+  positivity
+
+/-!
+
+## B. Integrals over one-dimensional space
+
+-/
+
+lemma integral_one_dim_eq_integral_real {f : Space 1 → ℝ} :
+    ∫ x, f x ∂volume = ∫ x, f (oneEquiv.symm x) ∂volume := by rw [integral_comp]
+
+/-!
+
+## C. Integrals over volume to spherical
+
+-/
+
+lemma integral_volume_eq_spherical (d : ℕ) (f : Space d.succ → F)
+    [NormedAddCommGroup F] [NormedSpace ℝ F] :
+    ∫ x, f x ∂volume = ∫ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d.succ).toSphere.prod
+        (Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by
+  rw [← MeasureTheory.MeasurePreserving.integral_comp (f := homeomorphUnitSphereProd _)
+    (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
+    (volume (α := Space d.succ)))
+    (Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d.succ)))]
+  simp only [Nat.succ_eq_add_one, homeomorphUnitSphereProd_apply_snd_coe,
+    homeomorphUnitSphereProd_apply_fst_coe]
+  let f' : (x : (Space d.succ)) → F := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)
+  conv_rhs =>
+    enter [2, x]
+    change f' x.1
+  rw [MeasureTheory.integral_subtype_comap (by simp), ← setIntegral_univ]
+  simp [f']
+  refine integral_congr_ae ?_
+  have h1 : ∀ᵐ x ∂(volume (α := Space d.succ)), x ≠ 0 := by
+    exact Measure.ae_ne volume 0
+  filter_upwards [Measure.ae_ne volume 0] with x hx
+  congr
+  simp [smul_smul]
+  have hx : ‖x‖ ≠ 0 := by
+    simpa using hx
+  field_simp
+  simp
+
+/- An instance of `sfinite` on the spherical integral measure on `Space d`.
+  This is needed in many of the calculations related to spherical integrals,
+  but cannot be inferred by Lean without this. -/
+instance : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpace
+        Real.measureSpace.toMeasurableSpace Subtype.val volume) := by
+      refine { out' := ?_ }
+      have h1 := SFinite.out' (μ := volume (α := ℝ))
+      obtain ⟨m, h⟩ := h1
+      use fun n => Measure.comap Subtype.val (m n)
+      apply And.intro
+      · intro n
+        refine (isFiniteMeasure_iff (Measure.comap Subtype.val (m n))).mpr ?_
+        rw [MeasurableEmbedding.comap_apply (MeasurableEmbedding.subtype_coe measurableSet_Ioi)]
+        simp only [Set.image_univ, Subtype.range_coe_subtype, Set.mem_Ioi]
+        have hm := h.1 n
+        exact measure_lt_top (m n) {x | 0 < x}
+      · ext s hs
+        rw [MeasurableEmbedding.comap_apply, Measure.sum_apply]
+        conv_rhs =>
+          enter [1, i]
+          rw [MeasurableEmbedding.comap_apply (MeasurableEmbedding.subtype_coe measurableSet_Ioi)]
+        have h2 := h.2
+        rw [Measure.ext_iff'] at h2
+        rw [← Measure.sum_apply]
+        exact h2 (Subtype.val '' s)
+        refine MeasurableSet.subtype_image measurableSet_Ioi hs
+        exact hs
+        apply MeasurableEmbedding.subtype_coe
+        simp
+
+/-!
+
+## D. Lower Lebesgue integral over volume to spherical
+
+-/
+
+lemma lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) :
+    ∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d.succ).toSphere.prod
+        (Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by
+  have h0 := MeasureTheory.MeasurePreserving.lintegral_comp
+    (f := fun x => f (x.2.1 • x.1.1)) (g := homeomorphUnitSphereProd _)
+    (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
+    (volume (α := Space d.succ)))
+    (by fun_prop)
+  rw [← h0]
+  simp only [Nat.succ_eq_add_one, homeomorphUnitSphereProd_apply_snd_coe,
+    homeomorphUnitSphereProd_apply_fst_coe]
+  let f' : (x : (Space d.succ)) → ENNReal := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x)
+  conv_rhs =>
+    enter [2, x]
+    change f' x.1
+  rw [MeasureTheory.lintegral_subtype_comap (by simp)]
+  simp [f']
+  refine lintegral_congr_ae ?_
+  filter_upwards [Measure.ae_ne volume 0] with x hx
+  congr
+  simp [smul_smul]
+  have hx : ‖x‖ ≠ 0 := by
+    simpa using hx
+  field_simp
+  rw [one_smul]
+
+lemma lintegral_volume_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) :
+    ∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) * .ofReal (x.2.1 ^ d)
+      ∂(volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0)) := by
+  rw [lintegral_volume_eq_spherical, Measure.volumeIoiPow,
+    MeasureTheory.prod_withDensity_right,
+    MeasureTheory.lintegral_withDensity_eq_lintegral_mul,
+    Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right,
+    MeasureTheory.lintegral_withDensity_eq_lintegral_mul]
+  · refine lintegral_congr_ae ?_
+    simp only [Nat.succ_eq_add_one, finrank_eq_dim, add_tsub_cancel_right, pow_zero,
+      ENNReal.ofReal_one]
+    filter_upwards with x
+    simp only [Pi.mul_apply, one_mul]
+    ring
+  all_goals fun_prop
+
+end Space
diff --git a/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
new file mode 100644
index 00000000..dba7385a
--- /dev/null
+++ b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
@@ -0,0 +1,314 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import PhysLean.Mathematics.Distribution.Basic
+import PhysLean.SpaceAndTime.Space.Integrals.Basic
+/-!
+
+# The radial angular measure on Space
+
+## i. Overview
+
+The normal measure on `Space d` is `r^(d-1) dr dΩ` in spherical coordinates,
+where `dΩ` is the angular measure on the unit sphere. The radial angular measure
+is the measure `dr dΩ`, cancelling the radius contribution from the measure in spherical
+coordinates.
+
+This file is equivalent to `invPowMeasure`, which will slowly be deprecated.
+
+## ii. Key results
+
+- `radialAngularMeasure`: The radial angular measure on `Space d`.
+
+## iii. Table of contents
+
+- A. The definition of the radial angular measure
+  - A.1. Basic equalities
+- B. Integrals with respect to radialAngularMeasure
+- C. The radialAngularMeasure on balls
+- D. Integrability conditions
+- E. HasTemperateGrowth of measures
+  - E.1. Integrability of powers
+  - E.2. radialAngularMeasure has temperate growth
+
+## iv. References
+
+-/
+open SchwartzMap NNReal Real
+noncomputable section
+
+variable (𝕜 : Type) {E F F' : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F]
+  [NormedAddCommGroup F']
+
+variable [NormedSpace ℝ E] [NormedSpace ℝ F]
+
+namespace Space
+
+open MeasureTheory
+
+/-!
+
+## A. The definition of the radial angular measure
+
+-/
+
+/-- The measure on `Space d` weighted by `1 / ‖x‖ ^ (d - 1)`. -/
+def radialAngularMeasure {d : ℕ} : Measure (Space d) :=
+  volume.withDensity (fun x : Space d => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)))
+
+/-!
+
+### A.1. Basic equalities
+
+-/
+
+lemma radialAngularMeasure_eq_volume_withDensity {d : ℕ} : radialAngularMeasure =
+    volume.withDensity (fun x : Space d => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) := by
+  rfl
+
+@[simp]
+lemma radialAngularMeasure_zero_eq_volume :
+    radialAngularMeasure (d := 0) = volume := by
+  simp [radialAngularMeasure]
+
+/-!
+
+### A.2. SFinite property
+
+-/
+
+instance (d : ℕ) : SFinite (radialAngularMeasure (d := d)) := by
+  dsimp [radialAngularMeasure]
+  infer_instance
+
+/-!
+
+## B. Integrals with respect to radialAngularMeasure
+
+-/
+
+lemma integral_radialAngularMeasure {d : ℕ} (f : Space d → F) :
+    ∫ x, f x ∂radialAngularMeasure = ∫ x, (1 / ‖x‖ ^ (d - 1)) • f x := by
+  dsimp [radialAngularMeasure]
+  erw [integral_withDensity_eq_integral_smul (by fun_prop)]
+  congr
+  funext x
+  simp only [one_div]
+  refine Eq.symm (Mathlib.Tactic.LinearCombination.smul_eq_const ?_ (f x))
+  simp
+
+lemma lintegral_radialMeasure {d : ℕ} (f : Space d → ENNReal) (hf : Measurable f) :
+    ∫⁻ x, f x ∂radialAngularMeasure = ∫⁻ x, ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f x := by
+  dsimp [radialAngularMeasure]
+  rw [lintegral_withDensity_eq_lintegral_mul]
+  simp only [one_div, Pi.mul_apply]
+  · fun_prop
+  · fun_prop
+
+lemma lintegral_radialMeasure_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal)
+    (hf : Measurable f) :
+    ∫⁻ x, f x ∂radialAngularMeasure = ∫⁻ x, f (x.2.1 • x.1.1)
+      ∂(volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0)) := by
+  rw [lintegral_radialMeasure, lintegral_volume_eq_spherical_mul]
+  apply lintegral_congr_ae
+  filter_upwards with x
+  have hx := x.2.2
+  simp [Nat.succ_eq_add_one, -Subtype.coe_prop] at hx
+  simp [norm_smul]
+  rw [abs_of_nonneg (le_of_lt x.2.2)]
+  trans ENNReal.ofReal (↑x.2 ^ d * (x.2.1 ^ d)⁻¹) * f (x.2.1 • ↑x.1.1)
+  · rw [ENNReal.ofReal_mul]
+    ring
+    have h2 := x.2.2
+    simp at h2
+    positivity
+  trans ENNReal.ofReal 1 * f (x.2.1 • ↑x.1.1)
+  · congr
+    field_simp
+  simp only [ENNReal.ofReal_one, Nat.succ_eq_add_one, one_mul]
+  fun_prop
+  fun_prop
+
+/-!
+
+## C. The radialAngularMeasure on balls
+
+-/
+
+@[simp]
+lemma radialAngularMeasure_closedBall (r : ℝ) :
+    radialAngularMeasure (Metric.closedBall (0 : Space 3) r) = ENNReal.ofReal (4 * π * r) := by
+  rw [← setLIntegral_one, ← MeasureTheory.lintegral_indicator measurableSet_closedBall,
+    lintegral_radialMeasure_eq_spherical_mul _ _
+    ((measurable_indicator_const_iff 1).mpr measurableSet_closedBall)]
+  have h1 (x : (Metric.sphere (0 : Space) 1) × ↑(Set.Ioi (0 : ℝ))) :
+      (Metric.closedBall (0 : Space) r).indicator (fun x => (1 : ENNReal)) (x.2.1 • x.1.1) =
+      (Set.univ ×ˢ {a | a.1 ≤ r}).indicator (fun x => 1) x :=
+      Set.indicator_const_eq_indicator_const <| by
+    simp [norm_smul]
+    rw [abs_of_nonneg (le_of_lt x.2.2)]
+  simp [h1]
+  rw [MeasureTheory.lintegral_indicator <|
+    MeasurableSet.prod MeasurableSet.univ (measurableSet_setOf.mpr (by fun_prop))]
+  simp [MeasureTheory.Measure.prod_prod, Measure.volumeIoiPow]
+  rw [MeasureTheory.Measure.comap_apply _ Subtype.val_injective
+    (fun s hs => MeasurableSet.subtype_image measurableSet_Ioi hs)
+    _ (measurableSet_setOf.mpr (by fun_prop))]
+  trans 3 * ENNReal.ofReal (4 / 3 * π) * volume (α := ℝ) (Set.Ioc 0 r)
+  · congr
+    ext x
+    simp only [Set.mem_image, Set.mem_setOf_eq, Subtype.exists, Set.mem_Ioi, exists_and_left,
+      exists_prop, exists_eq_right_right, Set.mem_Ioc]
+    grind
+  simp only [volume_Ioc, sub_zero]
+  trans ENNReal.ofReal (3 * ((4 / 3 * π))) * ENNReal.ofReal r
+  · simp [ENNReal.ofReal_mul]
+  field_simp
+  rw [← ENNReal.ofReal_mul (by positivity)]
+
+lemma radialAngularMeasure_real_closedBall (r : ℝ) (hr : 0 < r) :
+    radialAngularMeasure.real (Metric.closedBall (0 : Space 3) r) = 4 * π * r := by
+  change (radialAngularMeasure (Metric.closedBall (0 : Space 3) r)).toReal = _
+  simp only [radialAngularMeasure_closedBall, ENNReal.toReal_ofReal_eq_iff]
+  positivity
+
+/-!
+
+## D. Integrability conditions
+
+-/
+
+lemma integrable_radialAngularMeasure_iff {d : ℕ} {f : Space d → F} :
+    Integrable f (radialAngularMeasure (d := d)) ↔
+      Integrable (fun x => (1 / ‖x‖ ^ (d - 1)) • f x) volume := by
+  dsimp [radialAngularMeasure]
+  erw [integrable_withDensity_iff_integrable_smul₀ (by fun_prop)]
+  simp only [one_div]
+  refine integrable_congr ?_
+  filter_upwards with x
+  rw [Real.toNNReal_of_nonneg (by positivity), NNReal.smul_def, coe_mk]
+
+omit [NormedSpace ℝ F] in
+lemma integrable_radialAngularMeasure_of_spherical {d : ℕ} (f : Space d.succ → F)
+    (hae : StronglyMeasurable f)
+    (hf : Integrable (fun x => f (x.2.1 • x.1.1))
+    (volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0))) :
+    Integrable f radialAngularMeasure := by
+  refine ⟨StronglyMeasurable.aestronglyMeasurable hae, ?_⟩
+  rw [hasFiniteIntegral_iff_norm, lintegral_radialMeasure_eq_spherical_mul _ _
+    (by simpa using StronglyMeasurable.enorm hae), ← hasFiniteIntegral_iff_norm]
+  exact hf.2
+
+/-!
+
+## E. HasTemperateGrowth of measures
+
+-/
+
+/-!
+
+### E.1. Integrability of powers
+
+-/
+private lemma integrable_neg_pow_on_ioi (n : ℕ) :
+    IntegrableOn (fun x : ℝ => (|((1 : ℝ) + x) ^ (- (n + 2) : ℝ)|)) (Set.Ioi 0) := by
+  rw [MeasureTheory.integrableOn_iff_comap_subtypeVal]
+  rw [← MeasureTheory.integrable_smul_measure (c := n + 1)]
+  apply MeasureTheory.integrable_of_integral_eq_one
+  trans (n + 1) * ∫ (x : ℝ) in Set.Ioi 0, ((1 + x) ^ (- (n + 2) : ℝ)) ∂volume
+  · rw [← MeasureTheory.integral_subtype_comap measurableSet_Ioi]
+    simp only [neg_add_rev, Function.comp_apply, integral_smul_measure, smul_eq_mul]
+    congr
+    funext x
+    simp only [abs_eq_self]
+    apply Real.rpow_nonneg
+    grind
+  have h0 (x : ℝ) (hx : x ∈ Set.Ioi 0) : ((1 : ℝ) + ↑x) ^ (- (n + 2) : ℝ) =
+      ((1 + x) ^ ((n + 2)))⁻¹ := by
+    rw [← Real.rpow_natCast, ← Real.inv_rpow, ← Real.rpow_neg_one, ← Real.rpow_mul]
+    · simp [neg_add_rev, Nat.cast_add, Nat.cast_ofNat]
+    · rw [Set.mem_Ioi] at hx
+      positivity
+    · grind
+  trans (n + 1) * ∫ (x : ℝ) in Set.Ioi 0, ((1 + x) ^ (n + 2))⁻¹ ∂volume
+  · congr 1
+    refine setIntegral_congr_ae₀ ?_ ?_
+    · simp
+    filter_upwards with x hx
+    rw [h0 x hx]
+  trans (n + 1) * ∫ (x : ℝ) in Set.Ioi 1, (x ^ (n + 2))⁻¹ ∂volume
+  · congr 1
+    let f := fun x : ℝ => (x ^ (n + 2))⁻¹
+    change ∫ (x : ℝ) in Set.Ioi 0, f (1 + x) ∂volume = ∫ (x : ℝ) in Set.Ioi 1, f x ∂volume
+    let fa := fun x : ℝ => 1 + x
+    change ∫ (x : ℝ) in Set.Ioi 0, f (fa x) ∂volume = _
+    rw [← MeasureTheory.MeasurePreserving.setIntegral_image_emb (ν := volume)]
+    · simp [fa]
+    · simpa [fa] using measurePreserving_add_left volume 1
+    · simpa [fa] using measurableEmbedding_addLeft 1
+  · trans (n + 1) * ∫ (x : ℝ) in Set.Ioi 1, (x ^ (- (n + 2) : ℝ)) ∂volume
+    · congr 1
+      refine setIntegral_congr_ae₀ ?_ ?_
+      · simp
+      filter_upwards with x hx
+      have hx : 1 < x := hx
+      rw [← Real.rpow_natCast, ← Real.inv_rpow, ← Real.rpow_neg_one, ← Real.rpow_mul]
+      · simp
+      · positivity
+      · positivity
+    rw [integral_Ioi_rpow_of_lt (by linarith) (by linarith)]
+    field_simp
+    have h0 : (-2 + -(n : ℝ) + 1) ≠ 0 := by
+      by_contra h
+      have h1 : (1 : ℝ) - 0 = 2 + n := by grind
+      simp at h1
+      linarith
+    simp only [neg_add_rev, Real.one_rpow, mul_one]
+    grind
+  · simp
+  · simp
+  · simp
+
+lemma radialAngularMeasure_integrable_pow_neg_two {d : ℕ} :
+    Integrable (fun x : Space d => (1 + ‖x‖) ^ (- (d + 1) : ℝ))
+      radialAngularMeasure := by
+  match d with
+  | 0 => simp
+  | dm1 + 1 =>
+  apply integrable_radialAngularMeasure_of_spherical _ (by fun_prop)
+  simp [norm_smul]
+  rw [MeasureTheory.integrable_prod_iff]
+  rotate_left
+  · apply AEMeasurable.aestronglyMeasurable
+    fun_prop
+  refine ⟨?_, by simp⟩
+  filter_upwards with x
+  simp [Measure.volumeIoiPow]
+  let f := fun x : ℝ => |(1 + x) ^ (- (dm1 + 2) : ℝ)|
+  have h0 : (fun (y : ↑(Set.Ioi 0)) => (1 + |y.1|) ^ (-1 + (-1 + -↑dm1) : ℝ)) =
+      f ∘ Subtype.val := by
+    funext x
+    rcases x with ⟨x, hx⟩
+    simp at hx
+    simp [f]
+    ring_nf
+    rw [abs_of_nonneg (by positivity), abs_of_nonneg (by positivity)]
+  rw [h0]
+  change Integrable (f ∘ Subtype.val) _
+  rw [← MeasureTheory.integrableOn_iff_comap_subtypeVal measurableSet_Ioi]
+  exact integrable_neg_pow_on_ioi dm1
+
+/-!
+
+### E.2. radialAngularMeasure has temperate growth
+
+-/
+
+instance (d : ℕ) : Measure.HasTemperateGrowth (radialAngularMeasure (d := d)) where
+  exists_integrable := by
+    use d + 1
+    simpa using radialAngularMeasure_integrable_pow_neg_two (d := d)
+
+end Space
diff --git a/PhysLean/SpaceAndTime/Space/IsDistBounded.lean b/PhysLean/SpaceAndTime/Space/IsDistBounded.lean
index 2de86070..98002f54 100644
--- a/PhysLean/SpaceAndTime/Space/IsDistBounded.lean
+++ b/PhysLean/SpaceAndTime/Space/IsDistBounded.lean
@@ -3,7 +3,7 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import PhysLean.SpaceAndTime.Space.RadialAngularMeasure
+import PhysLean.SpaceAndTime.Space.Integrals.RadialAngularMeasure
 import PhysLean.SpaceAndTime.Time.Derivatives
 import Mathlib.Tactic.Cases
 /-!
diff --git a/PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean b/PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean
deleted file mode 100644
index 0000e19f..00000000
--- a/PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean
+++ /dev/null
@@ -1,331 +0,0 @@
-/-
-Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joseph Tooby-Smith
--/
-import PhysLean.Mathematics.Distribution.Basic
-import PhysLean.SpaceAndTime.Space.Basic
-/-!
-
-# The radial angular measure on Space
-
-## i. Overview
-
-The normal measure on `Space d` is `r^(d-1) dr dΩ` in spherical coordinates,
-where `dΩ` is the angular measure on the unit sphere. The radial angular measure
-is the measure `dr dΩ`, cancelling the radius contribution from the measure in spherical
-coordinates.
-
-This file is equivalent to `invPowMeasure`, which will slowly be deprecated.
-
-## ii. Key results
-
-- `radialAngularMeasure`: The radial angular measure on `Space d`.
-
-## iii. Table of contents
-
-- A. The definition of the radial angular measure
-  - A.1. Basic equalities
-- B. Integrals with respect to radialAngularMeasure
-- C. HasTemperateGrowth of measures
-  - C.1. Integrability of powers
-  - C.2. radialAngularMeasure has temperate growth
-
-## iv. References
-
--/
-open SchwartzMap NNReal
-noncomputable section
-
-variable (𝕜 : Type) {E F F' : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F]
-  [NormedAddCommGroup F']
-
-variable [NormedSpace ℝ E] [NormedSpace ℝ F]
-
-namespace Space
-
-open MeasureTheory
-
-/-!
-
-## A. The definition of the radial angular measure
-
--/
-
-/-- The measure on `Space d` weighted by `1 / ‖x‖ ^ (d - 1)`. -/
-def radialAngularMeasure {d : ℕ} : Measure (Space d) :=
-  volume.withDensity (fun x : Space d => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)))
-
-/-!
-
-### A.1. Basic equalities
-
--/
-
-lemma radialAngularMeasure_eq_volume_withDensity {d : ℕ} : radialAngularMeasure =
-    volume.withDensity (fun x : Space d => ENNReal.ofReal (1 / ‖x‖ ^ (d - 1))) := by
-  rfl
-
-@[simp]
-lemma radialAngularMeasure_zero_eq_volume :
-    radialAngularMeasure (d := 0) = volume := by
-  simp [radialAngularMeasure]
-
-lemma integrable_radialAngularMeasure_iff {d : ℕ} {f : Space d → F} :
-    Integrable f (radialAngularMeasure (d := d)) ↔
-      Integrable (fun x => (1 / ‖x‖ ^ (d - 1)) • f x) volume := by
-  dsimp [radialAngularMeasure]
-  erw [integrable_withDensity_iff_integrable_smul₀ (by fun_prop)]
-  simp only [one_div]
-  refine integrable_congr ?_
-  filter_upwards with x
-  rw [Real.toNNReal_of_nonneg, NNReal.smul_def]
-  simp only [inv_nonneg, norm_nonneg, pow_nonneg, coe_mk]
-  positivity
-
-/-!
-
-## B. Integrals with respect to radialAngularMeasure
-
--/
-
-lemma integral_radialAngularMeasure {d : ℕ} (f : Space d → F) :
-    ∫ x, f x ∂radialAngularMeasure = ∫ x, (1 / ‖x‖ ^ (d - 1)) • f x := by
-  dsimp [radialAngularMeasure]
-  erw [integral_withDensity_eq_integral_smul (by fun_prop)]
-  congr
-  funext x
-  simp only [one_div]
-  refine Eq.symm (Mathlib.Tactic.LinearCombination.smul_eq_const ?_ (f x))
-  simp
-
-/-!
-
-## C. HasTemperateGrowth of measures
-
--/
-
-/-!
-
-### C.1. Integrability of powers
-
--/
-private lemma integrable_neg_pow_on_ioi (n : ℕ) :
-    IntegrableOn (fun x : ℝ => (|((1 : ℝ) + ↑x) ^ (- (n + 2) : ℝ)|)) (Set.Ioi 0) := by
-  rw [MeasureTheory.integrableOn_iff_comap_subtypeVal]
-  rw [← MeasureTheory.integrable_smul_measure (c := n + 1)]
-  apply MeasureTheory.integrable_of_integral_eq_one
-  trans (n + 1) * ∫ (x : ℝ) in Set.Ioi 0, ((1 + x) ^ (- (n + 2) : ℝ)) ∂volume
-  · rw [← MeasureTheory.integral_subtype_comap]
-    simp only [neg_add_rev, Function.comp_apply, integral_smul_measure, smul_eq_mul]
-    congr
-    funext x
-    simp only [abs_eq_self]
-    apply Real.rpow_nonneg
-    apply add_nonneg
-    · exact zero_le_one' ℝ
-    · exact le_of_lt x.2
-    exact measurableSet_Ioi
-  have h0 (x : ℝ) (hx : x ∈ Set.Ioi 0) : ((1 : ℝ) + ↑x) ^ (- (n + 2) : ℝ) =
-      ((1 + x) ^ ((n + 2)))⁻¹ := by
-    rw [← Real.rpow_natCast]
-    rw [← Real.inv_rpow]
-    rw [← Real.rpow_neg_one, ← Real.rpow_mul]
-    simp only [neg_mul, one_mul]
-    simp only [neg_add_rev, Nat.cast_add, Nat.cast_ofNat]
-    have hx : 0 < x := hx
-    positivity
-    apply add_nonneg
-    · exact zero_le_one' ℝ
-    · exact le_of_lt hx
-  trans (n + 1) * ∫ (x : ℝ) in Set.Ioi 0, ((1 + x) ^ (n + 2))⁻¹ ∂volume
-  · congr 1
-    refine setIntegral_congr_ae₀ ?_ ?_
-    · simp
-    filter_upwards with x hx
-    rw [h0 x hx]
-  trans (n + 1) * ∫ (x : ℝ) in Set.Ioi 1, (x ^ (n + 2))⁻¹ ∂volume
-  · congr 1
-    let f := fun x : ℝ => (x ^ (n + 2))⁻¹
-    change ∫ (x : ℝ) in Set.Ioi 0, f (1 + x) ∂volume = ∫ (x : ℝ) in Set.Ioi 1, f x ∂volume
-    let fa := fun x : ℝ => 1 + x
-    change ∫ (x : ℝ) in Set.Ioi 0, f (fa x) ∂volume = _
-    rw [← MeasureTheory.MeasurePreserving.setIntegral_image_emb (ν := volume)]
-    simp [fa]
-    simp [fa]
-    exact measurePreserving_add_left volume 1
-    simp [fa]
-    exact measurableEmbedding_addLeft 1
-  · trans (n + 1) * ∫ (x : ℝ) in Set.Ioi 1, (x ^ (- (n + 2) : ℝ)) ∂volume
-    · congr 1
-      refine setIntegral_congr_ae₀ ?_ ?_
-      · simp
-      filter_upwards with x hx
-      have hx : 1 < x := hx
-      rw [← Real.rpow_natCast]
-      rw [← Real.inv_rpow]
-      rw [← Real.rpow_neg_one, ← Real.rpow_mul]
-      simp only [neg_mul, one_mul]
-      simp only [Nat.cast_add, Nat.cast_ofNat, neg_add_rev]
-      positivity
-      positivity
-    rw [integral_Ioi_rpow_of_lt]
-    field_simp
-    have h0 : (-2 + -(n : ℝ) + 1) ≠ 0 := by
-      by_contra h
-      have h1 : (1 : ℝ) - 0 = 2 + n := by
-        rw [← h]
-        ring
-      simp at h1
-      linarith
-    simp only [neg_add_rev, Real.one_rpow, mul_one]
-    field_simp
-    ring
-    linarith
-    linarith
-  · simp
-  · simp
-  · simp
-
-lemma radialAngularMeasure_integrable_pow_neg_two {d : ℕ} :
-    Integrable (fun x : Space d => (1 + ‖x‖) ^ (- (d + 1) : ℝ))
-      radialAngularMeasure := by
-  match d with
-  | 0 => simp
-  | dm1 + 1 =>
-  suffices h1 : Integrable (fun x => (1 + ‖x‖) ^ (-(dm1 + 2) : ℝ)) radialAngularMeasure by
-    convert h1 using 3
-    grind
-  simp [radialAngularMeasure]
-  rw [MeasureTheory.integrable_withDensity_iff]
-  swap
-  · fun_prop
-  swap
-  · rw [@ae_iff]
-    simp
-  conv =>
-    enter [1, i]
-    rw [ENNReal.toReal_ofReal (by positivity)]
-  have h1 := (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
-    (volume (α := Space dm1.succ)))
-  have h2 : IntegrableOn (fun x : Space dm1.succ =>
-      ((1 + ‖x‖) ^ (- (dm1 + 2) : ℝ)) * (‖x‖ ^ dm1)⁻¹) {0}ᶜ := by
-    rw [MeasureTheory.integrableOn_iff_comap_subtypeVal]
-    swap
-    · refine MeasurableSet.compl_iff.mpr ?_
-      simp
-    let f := (fun x :Space dm1.succ =>
-        ((1 + ‖x‖) ^ (- (dm1 + 2) : ℝ)) * (‖x‖ ^ dm1)⁻¹)
-      ∘ @Subtype.val (Space dm1.succ) fun x =>
-        (@Membership.mem (Space dm1.succ)
-          (Set (Space dm1.succ)) Set.instMembership {0}ᶜ x)
-    have hf : (f ∘ (homeomorphUnitSphereProd (Space dm1.succ)).symm)∘
-      (homeomorphUnitSphereProd (Space dm1.succ)) = f := by
-      funext x
-      simp
-    change Integrable f _
-    rw [← hf]
-    refine (h1.integrable_comp_emb ?_).mpr ?_
-    · exact Homeomorph.measurableEmbedding
-        (homeomorphUnitSphereProd (Space dm1.succ))
-    haveI sfinite : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpace
-        Real.measureSpace.toMeasurableSpace Subtype.val volume) := by
-      refine { out' := ?_ }
-      have h1 := SFinite.out' (μ := volume (α := ℝ))
-      obtain ⟨m, h⟩ := h1
-      use fun n => Measure.comap Subtype.val (m n)
-      apply And.intro
-      · intro n
-        refine (isFiniteMeasure_iff (Measure.comap Subtype.val (m n))).mpr ?_
-        rw [MeasurableEmbedding.comap_apply]
-        simp only [Set.image_univ, Subtype.range_coe_subtype, Set.mem_Ioi]
-        have hm := h.1 n
-        exact measure_lt_top (m n) {x | 0 < x}
-        exact MeasurableEmbedding.subtype_coe measurableSet_Ioi
-      · ext s hs
-        rw [MeasurableEmbedding.comap_apply, Measure.sum_apply]
-        conv_rhs =>
-          enter [1, i]
-          rw [MeasurableEmbedding.comap_apply (MeasurableEmbedding.subtype_coe measurableSet_Ioi)]
-        have h2 := h.2
-        rw [Measure.ext_iff'] at h2
-        rw [← Measure.sum_apply]
-        exact h2 (Subtype.val '' s)
-        refine MeasurableSet.subtype_image measurableSet_Ioi hs
-        exact hs
-        exact MeasurableEmbedding.subtype_coe measurableSet_Ioi
-    have hf' : (f ∘ (homeomorphUnitSphereProd (Space dm1.succ)).symm) =
-      fun x =>((1 + x.2.val) ^ (- (dm1 + 2) : ℝ)) * (x.2.val ^ dm1)⁻¹ := by
-      funext x
-      simp only [Function.comp_apply, homeomorphUnitSphereProd_symm_apply_coe, f]
-      rw [norm_smul]
-      simp only [Real.norm_eq_abs, norm_eq_of_mem_sphere, mul_one]
-      rw [abs_of_nonneg (le_of_lt x.2.2)]
-    rw [hf']
-    simp [Measure.volumeIoiPow]
-    rw [MeasureTheory.prod_withDensity_right]
-    swap
-    · fun_prop
-    rw [MeasureTheory.integrable_withDensity_iff]
-    swap
-    · refine Measurable.ennreal_ofReal ?_
-      refine Measurable.pow_const ?_ dm1
-      apply Measurable.comp
-      · exact measurable_subtype_coe
-      · exact measurable_snd
-    swap
-    · apply Filter.Eventually.of_forall
-      intro x
-      exact ENNReal.ofReal_lt_top
-    have hf'' : (fun (x : ↑(Metric.sphere (α := (Space dm1.succ)) 0 1) ×
-        ↑(Set.Ioi (α := ℝ) 0)) =>
-        (((1 + x.2.val) ^ (- (dm1 + 2) : ℝ)) * (x.2.val ^ dm1)⁻¹ *
-          (ENNReal.ofReal (↑x.2.val ^ dm1)).toReal))
-        = fun x => ((1 + x.2.val) ^ (- (dm1 + 2) : ℝ)) := by
-      funext x
-      rw [ENNReal.toReal_ofReal]
-      generalize (1 + ↑x.2.val)= l
-      ring_nf
-      have h2 : x.2.val ≠ 0 := by
-        have h' := x.2.2
-        simp [- Subtype.coe_prop] at h'
-        linarith
-      field_simp
-      ring_nf
-      simp only [Nat.succ_eq_add_one, inv_pow]
-      field_simp
-      exact pow_nonneg (le_of_lt x.2.2) dm1
-    simp at hf''
-    rw [hf'']
-    apply (MeasureTheory.integrable_prod_iff' ?_).mpr ?_
-    · refine aestronglyMeasurable_iff_aemeasurable.mpr ?_
-      fun_prop
-    · simp
-      apply Integrable.const_mul
-      have h1 := integrable_neg_pow_on_ioi dm1
-      rw [MeasureTheory.integrableOn_iff_comap_subtypeVal] at h1
-      simpa using h1
-      exact measurableSet_Ioi
-  rw [← MeasureTheory.integrableOn_univ]
-  simp only [Nat.succ_eq_add_one, neg_add_rev] at h2
-  apply MeasureTheory.IntegrableOn.congr_set_ae h2
-  rw [← MeasureTheory.ae_eq_set_compl]
-  trans (∅ : Set (Space dm1.succ))
-  · apply Filter.EventuallyEq.of_eq
-    rw [← Set.compl_empty]
-    exact compl_compl _
-  · symm
-    simp
-
-/-!
-
-### C.2. radialAngularMeasure has temperate growth
-
--/
-
-instance (d : ℕ) : Measure.HasTemperateGrowth (radialAngularMeasure (d := d)) where
-  exists_integrable := by
-    use d + 1
-    simpa using radialAngularMeasure_integrable_pow_neg_two (d := d)
-
-end Space
diff --git a/PhysLean/SpaceAndTime/SpaceTime/Basic.lean b/PhysLean/SpaceAndTime/SpaceTime/Basic.lean
index 1ff5048b..24420d5b 100644
--- a/PhysLean/SpaceAndTime/SpaceTime/Basic.lean
+++ b/PhysLean/SpaceAndTime/SpaceTime/Basic.lean
@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 import PhysLean.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct
 import PhysLean.Relativity.SpeedOfLight
 import PhysLean.SpaceAndTime.Time.Basic
+import PhysLean.SpaceAndTime.Space.Integrals.Basic
 /-!
 # Spacetime