From 8b8cbe71ea52a3a870e921e2d53ba4fbee99db19 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 19 Feb 2026 09:02:57 +0000
Subject: [PATCH 1/5] feat: Create Integrals directory

---
 PhysLean.lean                                 |   3 +-
 PhysLean/SpaceAndTime/Space/Basic.lean        |  64 ----
 .../SpaceAndTime/Space/Integrals/Basic.lean   | 236 +++++++++++++
 .../{ => Integrals}/RadialAngularMeasure.lean | 309 ++++++++++--------
 .../SpaceAndTime/Space/IsDistBounded.lean     |   2 +-
 PhysLean/SpaceAndTime/SpaceTime/Basic.lean    |   1 +
 6 files changed, 408 insertions(+), 207 deletions(-)
 create mode 100644 PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
 rename PhysLean/SpaceAndTime/Space/{ => Integrals}/RadialAngularMeasure.lean (53%)

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/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index 097d6618..754992ff 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -712,8 +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 := ?_ }
@@ -729,66 +727,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..5e1a1648
--- /dev/null
+++ b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
@@ -0,0 +1,236 @@
+/-
+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 t
+  he 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 (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
+
+@[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
+  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 infered 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]
+        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
+        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
+  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]
+  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
+  simp
+  simp
+
+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]
+  rw [Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right,
+    MeasureTheory.lintegral_withDensity_eq_lintegral_mul ]
+  rw [Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right,
+    MeasureTheory.lintegral_withDensity_eq_lintegral_mul ]
+  · refine lintegral_congr_ae ?_
+    simp
+    filter_upwards with x
+    simp
+    ring
+  all_goals
+  · fun_prop
+
+
+end Space
diff --git a/PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
similarity index 53%
rename from PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean
rename to PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
index 0000e19f..255d64ec 100644
--- a/PhysLean/SpaceAndTime/Space/RadialAngularMeasure.lean
+++ b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
@@ -4,7 +4,7 @@ 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
+import PhysLean.SpaceAndTime.Space.Integrals.Basic
 /-!
 
 # The radial angular measure on Space
@@ -27,14 +27,16 @@ This file is equivalent to `invPowMeasure`, which will slowly be deprecated.
 - 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
+- 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
+open SchwartzMap NNReal Real
 noncomputable section
 
 variable (𝕜 : Type) {E F F' : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F]
@@ -71,17 +73,16 @@ 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
+
+/-!
+
+### A.2.  SFinite property
+
+-/
+
+instance (d : ℕ) : SFinite (radialAngularMeasure (d := d)):= 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
+  infer_instance
 
 /-!
 
@@ -99,19 +100,143 @@ lemma integral_radialAngularMeasure {d : ℕ} (f : Space d → F) :
   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
+  · 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
+  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,
+    lintegral_radialMeasure_eq_spherical_mul]
+  rotate_left
+  · refine (measurable_indicator_const_iff 1).mpr ?_
+    exact measurableSet_closedBall
+  · exact 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 := by
+    refine Set.indicator_const_eq_indicator_const ?_
+    simp [norm_smul]
+    rw [abs_of_nonneg (le_of_lt x.2.2)]
+  simp [h1]
+  rw [MeasureTheory.lintegral_indicator, setLIntegral_one]
+  rotate_left
+  · refine MeasurableSet.prod ?_ ?_
+    · exact MeasurableSet.univ
+    · simp
+      fun_prop
+  rw [MeasureTheory.Measure.prod_prod]
+  simp [Measure.volumeIoiPow]
+  rw [MeasureTheory.Measure.comap_apply]
+  rotate_left
+  · exact Subtype.val_injective
+  · intro s hs
+    refine MeasurableSet.subtype_image ?_ hs
+    exact measurableSet_Ioi
+  · simp
+    fun_prop
+  trans  3 * ENNReal.ofReal (4 / 3 * π) * volume (α := ℝ) (Set.Ioc 0 r)
+  · congr
+    ext x
+    simp
+    grind
+  simp
+  trans ENNReal.ofReal (3 *  ((4 / 3 * π) )) * ENNReal.ofReal r
+  · simp [ENNReal.ofReal_mul]
+  field_simp
+  rw [← ENNReal.ofReal_mul]
+  simp
+  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, NNReal.smul_def]
+  simp only [inv_nonneg, norm_nonneg, pow_nonneg, coe_mk]
+  positivity
+
+omit [NormedSpace ℝ F] in
+lemma integrable_radialAngularMeasure_of_spherical {d : ℕ} (f : Space d.succ → F)
+  (fae : AEStronglyMeasurable f radialAngularMeasure)
+  (ht : 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
+  have h1 := hf.1
+  have h2 := hf.2
+  refine ⟨fae, ?_⟩
+  · rw [hasFiniteIntegral_iff_norm]
+    rw [lintegral_radialMeasure_eq_spherical_mul]
+    rw [← hasFiniteIntegral_iff_norm]
+    exact h2
+    · simp
+      refine StronglyMeasurable.enorm ht
+
 /-!
 
-## C. HasTemperateGrowth of measures
+## E. HasTemperateGrowth of measures
 
 -/
 
 /-!
 
-### C.1. Integrability of powers
+### E.1. Integrability of powers
 
 -/
 private lemma integrable_neg_pow_on_ioi (n : ℕ) :
-    IntegrableOn (fun x : ℝ => (|((1 : ℝ) + ↑x) ^ (- (n + 2) : ℝ)|)) (Set.Ioi 0) := by
+    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
@@ -193,133 +318,35 @@ lemma radialAngularMeasure_integrable_pow_neg_two {d : ℕ} :
   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
+  apply integrable_radialAngularMeasure_of_spherical
+  · apply AEMeasurable.aestronglyMeasurable
+    fun_prop
   · 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
+  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
 
 /-!
 
-### C.2. radialAngularMeasure has temperate growth
+### E.2. radialAngularMeasure has temperate growth
 
 -/
 
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/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
 

From 690c237d59de42050770b51b3ed75a1c0d19b222 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 19 Feb 2026 09:07:23 +0000
Subject: [PATCH 2/5] refactor: Style lint

---
 .../SpaceAndTime/Space/Integrals/Basic.lean     | 13 ++++++++-----
 .../Space/Integrals/RadialAngularMeasure.lean   | 17 +++++++++--------
 2 files changed, 17 insertions(+), 13 deletions(-)

diff --git a/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
index 5e1a1648..38c430d4 100644
--- a/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
@@ -134,7 +134,8 @@ lemma integral_volume_eq_spherical (d : ℕ) (f : Space d.succ → F)
     (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd
     (volume (α := Space d.succ)))
     (Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d.succ)))]
-  simp
+  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]
@@ -199,7 +200,8 @@ lemma lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf
     (volume (α := Space d.succ)))
     (by fun_prop)
   rw [← h0]
-  simp
+  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]
@@ -213,7 +215,7 @@ lemma lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf
   have hx : ‖x‖ ≠ 0 := by
     simpa using hx
   field_simp
-  simp
+  simp only [one_smul]
   simp
 
 lemma lintegral_volume_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) :
@@ -225,9 +227,10 @@ lemma lintegral_volume_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal)
   rw [Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right,
     MeasureTheory.lintegral_withDensity_eq_lintegral_mul ]
   · refine lintegral_congr_ae ?_
-    simp
+    simp only [Nat.succ_eq_add_one, finrank_eq_dim, add_tsub_cancel_right, pow_zero,
+      ENNReal.ofReal_one]
     filter_upwards with x
-    simp
+    simp only [Pi.mul_apply, one_mul]
     ring
   all_goals
   · fun_prop
diff --git a/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
index 255d64ec..974cf084 100644
--- a/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
+++ b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
@@ -104,7 +104,7 @@ lemma lintegral_radialMeasure {d : ℕ} (f : Space d → ENNReal) (hf : Measurab
     ∫⁻ x, f x ∂radialAngularMeasure = ∫⁻ x, ENNReal.ofReal (1 / ‖x‖ ^ (d - 1)) * f x := by
   dsimp [radialAngularMeasure]
   rw [lintegral_withDensity_eq_lintegral_mul]
-  simp
+  simp only [one_div, Pi.mul_apply]
   · fun_prop
   · fun_prop
 
@@ -128,7 +128,7 @@ lemma lintegral_radialMeasure_eq_spherical_mul (d : ℕ) (f : Space d.succ → E
   trans ENNReal.ofReal 1 * f (x.2.1 • ↑x.1.1)
   · congr
     field_simp
-  simp
+  simp only [ENNReal.ofReal_one, Nat.succ_eq_add_one, one_mul]
   fun_prop
   fun_prop
 
@@ -173,14 +173,15 @@ lemma radialAngularMeasure_closedBall (r : ℝ) :
   trans  3 * ENNReal.ofReal (4 / 3 * π) * volume (α := ℝ) (Set.Ioc 0 r)
   · congr
     ext x
-    simp
+    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
+  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]
-  simp
+  simp only [Nat.ofNat_pos, mul_nonneg_iff_of_pos_left]
   positivity
 
 lemma radialAngularMeasure_real_closedBall (r : ℝ) (hr : 0 < r) :
@@ -209,9 +210,9 @@ lemma integrable_radialAngularMeasure_iff {d : ℕ} {f : Space d → F} :
 
 omit [NormedSpace ℝ F] in
 lemma integrable_radialAngularMeasure_of_spherical {d : ℕ} (f : Space d.succ → F)
-  (fae : AEStronglyMeasurable f radialAngularMeasure)
-  (ht : StronglyMeasurable f)
-  (hf : Integrable (fun x => f (x.2.1 • x.1.1))
+    (fae : AEStronglyMeasurable f radialAngularMeasure)
+    (ht : 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
   have h1 := hf.1

From 6c134b5357aade48bed7a1ac6958b836718f99f9 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 19 Feb 2026 09:17:45 +0000
Subject: [PATCH 3/5] refactor: Lint

---
 .../HarmonicOscillator/Basic.lean             |  1 -
 .../PointParticle/ThreeDimension.lean         | 16 ++++++----------
 .../TwoHDM/Potential.lean                     |  2 +-
 PhysLean/SpaceAndTime/Space/Basic.lean        |  1 -
 .../SpaceAndTime/Space/Integrals/Basic.lean   | 15 ++++++---------
 .../Space/Integrals/RadialAngularMeasure.lean | 19 +++++++++----------
 6 files changed, 22 insertions(+), 32 deletions(-)

diff --git a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean
index 19275675..5d7b4a39 100644
--- a/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean
+++ b/PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean
@@ -110,7 +110,6 @@ structure HarmonicOscillator where
 
 namespace HarmonicOscillator
 
-
 variable (S : HarmonicOscillator)
 
 @[simp]
diff --git a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
index 85f8105e..7de9b213 100644
--- a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
+++ b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
@@ -288,16 +288,12 @@ lemma threeDimPointParticle_div_electricField {𝓕} (q : ℝ) (r₀ : Space 3)
   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 [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/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
index 11b2090a..edb9fa7e 100644
--- a/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
+++ b/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
@@ -216,7 +216,7 @@ def stabilityCounterExample : PotentialParameters := {(0 : PotentialParameters)
     𝓵₆ := -2
     𝓵₇ := -2}
 
-lemma stabilityCounterExample_ξ  :
+lemma stabilityCounterExample_ξ :
     stabilityCounterExample.ξ = fun
       | Sum.inl 0 => 0
       | Sum.inr 0 => 0
diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index 754992ff..c7d3c4b6 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -712,7 +712,6 @@ lemma oneEquiv_measurePreserving : MeasurePreserving oneEquiv volume volume :=
 lemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume volume := by
   exact LinearIsometryEquiv.measurePreserving oneEquiv.symm
 
-
 instance {d : ℕ} : Nontrivial (Space d.succ) := by
   refine { exists_pair_ne := ?_ }
   use 0, basis 0
diff --git a/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
index 38c430d4..46944ca2 100644
--- a/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
@@ -25,7 +25,6 @@ We focus here on the volume measure, which is the usual measure on `Space d`, i.
   with respect to the volume measure can be expressed as a lower Lebesgue integral over the unit
   sphere and the positive reals.
 
-
 -/
 
 namespace Space
@@ -117,7 +116,7 @@ lemma volume_metricBall_three_real :
 
 -/
 
-lemma integral_one_dim_eq_integral_real {f : Space 1 → ℝ}  :
+lemma integral_one_dim_eq_integral_real {f : Space 1 → ℝ} :
     ∫ x, f x ∂volume = ∫ x, f (oneEquiv.symm x) ∂volume := by rw [integral_comp]
 
 /-!
@@ -128,7 +127,7 @@ lemma integral_one_dim_eq_integral_real {f : Space 1 → ℝ}  :
 
 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
+    ∫ 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
@@ -155,7 +154,7 @@ lemma integral_volume_eq_spherical (d : ℕ) (f : Space d.succ → F)
 
 /- 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 infered by Lean without this. -/
+  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' := ?_ }
@@ -184,7 +183,6 @@ instance : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpac
         apply MeasurableEmbedding.subtype_coe
         simp
 
-
 /-!
 
 ## D. Lower Lebesgue integral over volume to spherical
@@ -192,7 +190,7 @@ instance : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpac
 -/
 
 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
+    ∫⁻ 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 _)
@@ -223,9 +221,9 @@ lemma lintegral_volume_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal)
       ∂(volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0)) := by
   rw [lintegral_volume_eq_spherical]
   rw [Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right,
-    MeasureTheory.lintegral_withDensity_eq_lintegral_mul ]
+    MeasureTheory.lintegral_withDensity_eq_lintegral_mul]
   rw [Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right,
-    MeasureTheory.lintegral_withDensity_eq_lintegral_mul ]
+    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]
@@ -235,5 +233,4 @@ lemma lintegral_volume_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal)
   all_goals
   · fun_prop
 
-
 end Space
diff --git a/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
index 974cf084..8af7d125 100644
--- a/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
+++ b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
@@ -73,14 +73,13 @@ lemma radialAngularMeasure_zero_eq_volume :
     radialAngularMeasure (d := 0) = volume := by
   simp [radialAngularMeasure]
 
-
 /-!
 
-### A.2.  SFinite property
+### A.2. SFinite property
 
 -/
 
-instance (d : ℕ) : SFinite (radialAngularMeasure (d := d)):= by
+instance (d : ℕ) : SFinite (radialAngularMeasure (d := d)) := by
   dsimp [radialAngularMeasure]
   infer_instance
 
@@ -116,10 +115,10 @@ lemma lintegral_radialMeasure_eq_spherical_mul (d : ℕ) (f : Space d.succ → E
   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 [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)
+  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
@@ -148,8 +147,8 @@ lemma radialAngularMeasure_closedBall (r : ℝ) :
     exact measurableSet_closedBall
   · exact 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 := by
+      (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 := by
     refine Set.indicator_const_eq_indicator_const ?_
     simp [norm_smul]
     rw [abs_of_nonneg (le_of_lt x.2.2)]
@@ -170,14 +169,14 @@ lemma radialAngularMeasure_closedBall (r : ℝ) :
     exact measurableSet_Ioi
   · simp
     fun_prop
-  trans  3 * ENNReal.ofReal (4 / 3 * π) * volume (α := ℝ) (Set.Ioc 0 r)
+  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
+  trans ENNReal.ofReal (3 * ((4 / 3 * π))) * ENNReal.ofReal r
   · simp [ENNReal.ofReal_mul]
   field_simp
   rw [← ENNReal.ofReal_mul]
@@ -339,7 +338,7 @@ lemma radialAngularMeasure_integrable_pow_neg_two {d : ℕ} :
     simp at hx
     simp [f]
     ring_nf
-    rw [abs_of_nonneg (by positivity), abs_of_nonneg (by positivity) ]
+    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]

From 5d9587ef61ef7528ac0373bba33f6f6ba9196d74 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 19 Feb 2026 12:15:17 +0000
Subject: [PATCH 4/5] refactor: Proof gold

---
 .../Space/Integrals/RadialAngularMeasure.lean | 36 +++++++------------
 1 file changed, 12 insertions(+), 24 deletions(-)

diff --git a/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
index 8af7d125..52e57402 100644
--- a/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
+++ b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
@@ -209,20 +209,18 @@ lemma integrable_radialAngularMeasure_iff {d : ℕ} {f : Space d → F} :
 
 omit [NormedSpace ℝ F] in
 lemma integrable_radialAngularMeasure_of_spherical {d : ℕ} (f : Space d.succ → F)
-    (fae : AEStronglyMeasurable f radialAngularMeasure)
-    (ht : StronglyMeasurable 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
   have h1 := hf.1
   have h2 := hf.2
-  refine ⟨fae, ?_⟩
-  · rw [hasFiniteIntegral_iff_norm]
-    rw [lintegral_radialMeasure_eq_spherical_mul]
-    rw [← hasFiniteIntegral_iff_norm]
-    exact h2
-    · simp
-      refine StronglyMeasurable.enorm ht
+  refine ⟨StronglyMeasurable.aestronglyMeasurable hae, ?_⟩
+  rw [hasFiniteIntegral_iff_norm]
+  rw [lintegral_radialMeasure_eq_spherical_mul]
+  rw [← hasFiniteIntegral_iff_norm]
+  exact h2
+  · simpa using StronglyMeasurable.enorm hae
 
 /-!
 
@@ -241,16 +239,13 @@ private lemma integrable_neg_pow_on_ioi (n : ℕ) :
   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]
+  · 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
-    apply add_nonneg
-    · exact zero_le_one' ℝ
-    · exact le_of_lt x.2
-    exact measurableSet_Ioi
+    grind
   have h0 (x : ℝ) (hx : x ∈ Set.Ioi 0) : ((1 : ℝ) + ↑x) ^ (- (n + 2) : ℝ) =
       ((1 + x) ^ ((n + 2)))⁻¹ := by
     rw [← Real.rpow_natCast]
@@ -260,9 +255,7 @@ private lemma integrable_neg_pow_on_ioi (n : ℕ) :
     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
+    grind
   trans (n + 1) * ∫ (x : ℝ) in Set.Ioi 0, ((1 + x) ^ (n + 2))⁻¹ ∂volume
   · congr 1
     refine setIntegral_congr_ae₀ ?_ ?_
@@ -298,14 +291,11 @@ private lemma integrable_neg_pow_on_ioi (n : ℕ) :
     field_simp
     have h0 : (-2 + -(n : ℝ) + 1) ≠ 0 := by
       by_contra h
-      have h1 : (1 : ℝ) - 0 = 2 + n := by
-        rw [← h]
-        ring
+      have h1 : (1 : ℝ) - 0 = 2 + n := by grind
       simp at h1
       linarith
     simp only [neg_add_rev, Real.one_rpow, mul_one]
-    field_simp
-    ring
+    grind
     linarith
     linarith
   · simp
@@ -319,8 +309,6 @@ lemma radialAngularMeasure_integrable_pow_neg_two {d : ℕ} :
   | 0 => simp
   | dm1 + 1 =>
   apply integrable_radialAngularMeasure_of_spherical
-  · apply AEMeasurable.aestronglyMeasurable
-    fun_prop
   · fun_prop
   simp [norm_smul]
   rw [MeasureTheory.integrable_prod_iff]

From 75ecc9937e1026721739097ff4701c9d9bfc9b0e Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 25 Feb 2026 11:13:37 +0000
Subject: [PATCH 5/5] refactor: Review comments

---
 .../PointParticle/ThreeDimension.lean         |  3 +-
 .../SpaceAndTime/Space/Integrals/Basic.lean   | 31 +++----
 .../Space/Integrals/RadialAngularMeasure.lean | 92 ++++++-------------
 3 files changed, 44 insertions(+), 82 deletions(-)

diff --git a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
index 7de9b213..301024f2 100644
--- a/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
+++ b/PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean
@@ -287,8 +287,7 @@ 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]
-  simp [smul_smul]
+  simp only [map_smul, smul_smul]
   ext η
   simp [constantTime_apply, diracDelta_apply, distTranslate_apply]
   left
diff --git a/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
index 46944ca2..e05b988e 100644
--- a/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
@@ -19,8 +19,8 @@ We focus here on the volume measure, which is the usual measure on `Space d`, i.
 - `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 t
-  he positive reals.
+  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.
@@ -40,7 +40,7 @@ open InnerProductSpace MeasureTheory
 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) :
+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
@@ -65,16 +65,14 @@ 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)]
+  · 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
-    simpa using hk
-  · rw [InnerProductSpace.volume_closedBall_of_dim_odd (k := k)]
+  · 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
-    simpa using hk
 
 @[simp]
 lemma volume_metricBall_three :
@@ -164,11 +162,10 @@ instance : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpac
       apply And.intro
       · intro n
         refine (isFiniteMeasure_iff (Measure.comap Subtype.val (m n))).mpr ?_
-        rw [MeasurableEmbedding.comap_apply]
+        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}
-        exact MeasurableEmbedding.subtype_coe measurableSet_Ioi
       · ext s hs
         rw [MeasurableEmbedding.comap_apply, Measure.sum_apply]
         conv_rhs =>
@@ -204,7 +201,7 @@ lemma lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf
   conv_rhs =>
     enter [2, x]
     change f' x.1
-  rw [MeasureTheory.lintegral_subtype_comap]
+  rw [MeasureTheory.lintegral_subtype_comap (by simp)]
   simp [f']
   refine lintegral_congr_ae ?_
   filter_upwards [Measure.ae_ne volume 0] with x hx
@@ -213,16 +210,15 @@ lemma lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf
   have hx : ‖x‖ ≠ 0 := by
     simpa using hx
   field_simp
-  simp only [one_smul]
-  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]
-  rw [Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right,
-    MeasureTheory.lintegral_withDensity_eq_lintegral_mul]
-  rw [Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right,
+  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,
@@ -230,7 +226,6 @@ lemma lintegral_volume_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal)
     filter_upwards with x
     simp only [Pi.mul_apply, one_mul]
     ring
-  all_goals
-  · fun_prop
+  all_goals fun_prop
 
 end Space
diff --git a/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
index 52e57402..dba7385a 100644
--- a/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
+++ b/PhysLean/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
@@ -140,35 +140,22 @@ lemma lintegral_radialMeasure_eq_spherical_mul (d : ℕ) (f : Space d.succ → E
 @[simp]
 lemma radialAngularMeasure_closedBall (r : ℝ) :
     radialAngularMeasure (Metric.closedBall (0 : Space 3) r) = ENNReal.ofReal (4 * π * r) := by
-  rw [← setLIntegral_one, ← MeasureTheory.lintegral_indicator,
-    lintegral_radialMeasure_eq_spherical_mul]
-  rotate_left
-  · refine (measurable_indicator_const_iff 1).mpr ?_
-    exact measurableSet_closedBall
-  · exact measurableSet_closedBall
+  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 := by
-    refine Set.indicator_const_eq_indicator_const ?_
+      (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, setLIntegral_one]
-  rotate_left
-  · refine MeasurableSet.prod ?_ ?_
-    · exact MeasurableSet.univ
-    · simp
-      fun_prop
-  rw [MeasureTheory.Measure.prod_prod]
-  simp [Measure.volumeIoiPow]
-  rw [MeasureTheory.Measure.comap_apply]
-  rotate_left
-  · exact Subtype.val_injective
-  · intro s hs
-    refine MeasurableSet.subtype_image ?_ hs
-    exact measurableSet_Ioi
-  · simp
-    fun_prop
+  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
@@ -179,9 +166,7 @@ lemma radialAngularMeasure_closedBall (r : ℝ) :
   trans ENNReal.ofReal (3 * ((4 / 3 * π))) * ENNReal.ofReal r
   · simp [ENNReal.ofReal_mul]
   field_simp
-  rw [← ENNReal.ofReal_mul]
-  simp only [Nat.ofNat_pos, mul_nonneg_iff_of_pos_left]
-  positivity
+  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
@@ -203,9 +188,7 @@ lemma integrable_radialAngularMeasure_iff {d : ℕ} {f : Space d → F} :
   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
+  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)
@@ -213,14 +196,10 @@ lemma integrable_radialAngularMeasure_of_spherical {d : ℕ} (f : Space d.succ 
     (hf : Integrable (fun x => f (x.2.1 • x.1.1))
     (volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0))) :
     Integrable f radialAngularMeasure := by
-  have h1 := hf.1
-  have h2 := hf.2
   refine ⟨StronglyMeasurable.aestronglyMeasurable hae, ?_⟩
-  rw [hasFiniteIntegral_iff_norm]
-  rw [lintegral_radialMeasure_eq_spherical_mul]
-  rw [← hasFiniteIntegral_iff_norm]
-  exact h2
-  · simpa using StronglyMeasurable.enorm hae
+  rw [hasFiniteIntegral_iff_norm, lintegral_radialMeasure_eq_spherical_mul _ _
+    (by simpa using StronglyMeasurable.enorm hae), ← hasFiniteIntegral_iff_norm]
+  exact hf.2
 
 /-!
 
@@ -248,14 +227,11 @@ private lemma integrable_neg_pow_on_ioi (n : ℕ) :
     grind
   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
-    grind
+    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₀ ?_ ?_
@@ -269,25 +245,20 @@ private lemma integrable_neg_pow_on_ioi (n : ℕ) :
     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
+    · 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]
-      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]
+      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
@@ -296,8 +267,6 @@ private lemma integrable_neg_pow_on_ioi (n : ℕ) :
       linarith
     simp only [neg_add_rev, Real.one_rpow, mul_one]
     grind
-    linarith
-    linarith
   · simp
   · simp
   · simp
@@ -308,8 +277,7 @@ lemma radialAngularMeasure_integrable_pow_neg_two {d : ℕ} :
   match d with
   | 0 => simp
   | dm1 + 1 =>
-  apply integrable_radialAngularMeasure_of_spherical
-  · fun_prop
+  apply integrable_radialAngularMeasure_of_spherical _ (by fun_prop)
   simp [norm_smul]
   rw [MeasureTheory.integrable_prod_iff]
   rotate_left