From 7af070318f8bc0652852310ec13ef7e8f7921ef5 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 13 Mar 2026 19:40:34 -0700
Subject: [PATCH 1/7] feat(Momentum): prove
 `momentumOperatorSchwartz_isSymmetric`

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
---
 .../DDimensions/Operators/Momentum.lean       | 85 +++++++++++++++----
 1 file changed, 70 insertions(+), 15 deletions(-)

diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
index 2f5ad1847..c897322ec 100644
--- a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -9,6 +9,7 @@ public import PhysLean.QuantumMechanics.DDimensions.Operators.Unbounded
 public import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
 public import PhysLean.QuantumMechanics.PlanckConstant
 public import PhysLean.SpaceAndTime.Space.Derivatives.Basic
+import Mathlib.Analysis.Calculus.FDeriv.Star
 /-!
 
 # Momentum operators
@@ -97,31 +98,85 @@ lemma momentumOperatorSqr_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
 
 -/
 
-open SpaceDHilbertSpace
+open SpaceDHilbertSpace MeasureTheory
+
+/-- The spatial derivative of a Schwartz function as a Schwartz function. -/
+private def derivSchwartz (j : Fin d) (f : 𝓢(Space d, ℂ)) : 𝓢(Space d, ℂ) :=
+  (SchwartzMap.evalCLM ℂ (Space d) ℂ (basis j))
+    ((SchwartzMap.fderivCLM ℂ (Space d) ℂ) f)
 
 /-- The momentum operators defined on the Schwartz submodule. -/
 def momentumOperatorSchwartz : schwartzSubmodule d →ₗ[ℂ] schwartzSubmodule d :=
   schwartzEquiv.toLinearMap ∘ₗ 𝐩[i].toLinearMap ∘ₗ schwartzEquiv.symm.toLinearMap
 
-@[sorryful]
-lemma momentumOperatorSchwartz_isSymmetric : (momentumOperatorSchwartz i).IsSymmetric := by
+lemma momentumOperatorSchwartz_isSymmetric :
+    (momentumOperatorSchwartz i).IsSymmetric := by
   intro ψ ψ'
   obtain ⟨f, rfl⟩ := schwartzEquiv.surjective ψ
   obtain ⟨f', rfl⟩ := schwartzEquiv.surjective ψ'
   unfold momentumOperatorSchwartz
   simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, ContinuousLinearMap.coe_coe,
-    Function.comp_apply, LinearEquiv.symm_apply_apply, schwartzEquiv_inner, momentumOperator_apply,
-    neg_mul, map_neg, map_mul, Complex.conj_I, Complex.conj_ofReal, neg_neg, mul_neg]
-  -- Need integration by parts and `starRingEnd ∂[i] = ∂[i] starRingEnd`:
-  -- ⊢ ∫ (x : Space d), Complex.I * ↑↑ℏ * (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x =
-  -- ∫ (x : Space d), -((starRingEnd ℂ) (f x) * (Complex.I * ↑↑ℏ * Space.deriv i (⇑f') x))
-  sorry
-
-/-- The symmetric momentum unbounded operators with domain the Schwartz submodule
-  of the Hilbert space. -/
-@[sorryful]
-def momentumUnboundedOperator : UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
-  UnboundedOperator.ofSymmetric (schwartzSubmodule_dense d) (momentumOperatorSchwartz_isSymmetric i)
+    Function.comp_apply, LinearEquiv.symm_apply_apply, schwartzEquiv_inner,
+    momentumOperator_apply, neg_mul, map_neg, map_mul, Complex.conj_I,
+    Complex.conj_ofReal, neg_neg, mul_neg]
+  rw [integral_neg]
+  simp_rw [show ∀ x : Space d, Complex.I * ↑↑ℏ *
+    (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x =
+    (Complex.I * ↑↑ℏ) *
+    ((starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x) from
+    fun x => by ring]
+  simp_rw [show ∀ x : Space d, (starRingEnd ℂ) (f x) *
+    (Complex.I * ↑↑ℏ * Space.deriv i (⇑f') x) =
+    (Complex.I * ↑↑ℏ) *
+    ((starRingEnd ℂ) (f x) * Space.deriv i (⇑f') x) from
+    fun x => by ring]
+  rw [integral_const_mul, integral_const_mul, neg_mul_eq_mul_neg]
+  congr 1
+  have hstar_fderiv : ∀ x : Space d,
+      (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x =
+      fderiv ℝ (fun y => star (f y)) x (basis i) * f' x := by
+    intro x; congr 1
+    change star (fderiv ℝ (⇑f) x (basis i)) = _
+    rw [fderiv_star (𝕜 := ℝ)]; simp
+  simp_rw [hstar_fderiv]
+  change ∫ x, fderiv ℝ (fun y => star (f y)) x (basis i) *
+    f' x = -(∫ x, star (f x) *
+    fderiv ℝ (⇑f') x (basis i))
+  have ibp := integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable
+    (f := fun x => star (f x)) (g := ⇑f') (v := basis i)
+    (μ := volume) (hf'g := ?_) (hfg' := ?_) (hfg := ?_)
+    (Differentiable.star (SchwartzMap.differentiable f))
+    (SchwartzMap.differentiable f')
+  · rw [ibp, neg_neg]
+  · have h : ∀ x, (fderiv ℝ (fun x => star (f x)) x)
+        (basis i) = star ((derivSchwartz i f) x) := by
+      intro x; rw [fderiv_star (𝕜 := ℝ)]; simp [derivSchwartz]
+    simp_rw [h]
+    exact Integrable.mul_of_top_left
+      ((ContinuousLinearEquiv.integrable_comp_iff
+        (starL' ℝ : ℂ ≃L[ℝ] ℂ)).mpr
+        (SchwartzMap.integrable (derivSchwartz i f)))
+      (SchwartzMap.memLp_top f' volume)
+  · have h : ∀ x, (fderiv ℝ (⇑f') x) (basis i) =
+        (derivSchwartz i f') x := fun _ => rfl
+    simp_rw [h]
+    exact Integrable.mul_of_top_left
+      ((ContinuousLinearEquiv.integrable_comp_iff
+        (starL' ℝ : ℂ ≃L[ℝ] ℂ)).mpr
+        (SchwartzMap.integrable f))
+      (SchwartzMap.memLp_top (derivSchwartz i f') volume)
+  · exact Integrable.mul_of_top_left
+      ((ContinuousLinearEquiv.integrable_comp_iff
+        (starL' ℝ : ℂ ≃L[ℝ] ℂ)).mpr
+        (SchwartzMap.integrable f))
+      (SchwartzMap.memLp_top f' volume)
+
+/-- The symmetric momentum unbounded operators with domain the Schwartz
+  submodule of the Hilbert space. -/
+def momentumUnboundedOperator :
+    UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
+  UnboundedOperator.ofSymmetric (schwartzSubmodule_dense d)
+    (momentumOperatorSchwartz_isSymmetric i)
 
 end
 end QuantumMechanics

From 175438bccec86f7aa9c68a82a8928518f5cb4695 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Mon, 16 Mar 2026 10:00:16 -0700
Subject: [PATCH 2/7] refactor(Momentum): remove private def derivSchwartz, use
 local let

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
---
 .../DDimensions/Operators/Momentum.lean        | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
index c897322ec..a72bca429 100644
--- a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -100,11 +100,6 @@ lemma momentumOperatorSqr_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) :
 
 open SpaceDHilbertSpace MeasureTheory
 
-/-- The spatial derivative of a Schwartz function as a Schwartz function. -/
-private def derivSchwartz (j : Fin d) (f : 𝓢(Space d, ℂ)) : 𝓢(Space d, ℂ) :=
-  (SchwartzMap.evalCLM ℂ (Space d) ℂ (basis j))
-    ((SchwartzMap.fderivCLM ℂ (Space d) ℂ) f)
-
 /-- The momentum operators defined on the Schwartz submodule. -/
 def momentumOperatorSchwartz : schwartzSubmodule d →ₗ[ℂ] schwartzSubmodule d :=
   schwartzEquiv.toLinearMap ∘ₗ 𝐩[i].toLinearMap ∘ₗ schwartzEquiv.symm.toLinearMap
@@ -132,6 +127,9 @@ lemma momentumOperatorSchwartz_isSymmetric :
     fun x => by ring]
   rw [integral_const_mul, integral_const_mul, neg_mul_eq_mul_neg]
   congr 1
+  let derivS (j : Fin d) (g : 𝓢(Space d, ℂ)) : 𝓢(Space d, ℂ) :=
+    (SchwartzMap.evalCLM ℂ (Space d) ℂ (basis j))
+      ((SchwartzMap.fderivCLM ℂ (Space d) ℂ) g)
   have hstar_fderiv : ∀ x : Space d,
       (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x =
       fderiv ℝ (fun y => star (f y)) x (basis i) * f' x := by
@@ -149,22 +147,22 @@ lemma momentumOperatorSchwartz_isSymmetric :
     (SchwartzMap.differentiable f')
   · rw [ibp, neg_neg]
   · have h : ∀ x, (fderiv ℝ (fun x => star (f x)) x)
-        (basis i) = star ((derivSchwartz i f) x) := by
-      intro x; rw [fderiv_star (𝕜 := ℝ)]; simp [derivSchwartz]
+        (basis i) = star ((derivS i f) x) := by
+      intro x; rw [fderiv_star (𝕜 := ℝ)]; simp [derivS]
     simp_rw [h]
     exact Integrable.mul_of_top_left
       ((ContinuousLinearEquiv.integrable_comp_iff
         (starL' ℝ : ℂ ≃L[ℝ] ℂ)).mpr
-        (SchwartzMap.integrable (derivSchwartz i f)))
+        (SchwartzMap.integrable (derivS i f)))
       (SchwartzMap.memLp_top f' volume)
   · have h : ∀ x, (fderiv ℝ (⇑f') x) (basis i) =
-        (derivSchwartz i f') x := fun _ => rfl
+        (derivS i f') x := fun _ => rfl
     simp_rw [h]
     exact Integrable.mul_of_top_left
       ((ContinuousLinearEquiv.integrable_comp_iff
         (starL' ℝ : ℂ ≃L[ℝ] ℂ)).mpr
         (SchwartzMap.integrable f))
-      (SchwartzMap.memLp_top (derivSchwartz i f') volume)
+      (SchwartzMap.memLp_top (derivS i f') volume)
   · exact Integrable.mul_of_top_left
       ((ContinuousLinearEquiv.integrable_comp_iff
         (starL' ℝ : ℂ ≃L[ℝ] ℂ)).mpr

From bfcb7e6eccd0a837a57fe1364f28c7bee58cee86 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 19 Mar 2026 20:43:37 +0100
Subject: [PATCH 3/7] golf(Momentum): shorten
 momentumOperatorSchwartz_isSymmetric proof

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
---
 .../DDimensions/Operators/Momentum.lean       | 75 +++++++------------
 1 file changed, 28 insertions(+), 47 deletions(-)

diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
index a72bca429..fcc70947c 100644
--- a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -116,57 +116,38 @@ lemma momentumOperatorSchwartz_isSymmetric :
     Complex.conj_ofReal, neg_neg, mul_neg]
   rw [integral_neg]
   simp_rw [show ∀ x : Space d, Complex.I * ↑↑ℏ *
-    (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x =
-    (Complex.I * ↑↑ℏ) *
-    ((starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x) from
-    fun x => by ring]
-  simp_rw [show ∀ x : Space d, (starRingEnd ℂ) (f x) *
-    (Complex.I * ↑↑ℏ * Space.deriv i (⇑f') x) =
-    (Complex.I * ↑↑ℏ) *
-    ((starRingEnd ℂ) (f x) * Space.deriv i (⇑f') x) from
-    fun x => by ring]
-  rw [integral_const_mul, integral_const_mul, neg_mul_eq_mul_neg]
-  congr 1
-  let derivS (j : Fin d) (g : 𝓢(Space d, ℂ)) : 𝓢(Space d, ℂ) :=
-    (SchwartzMap.evalCLM ℂ (Space d) ℂ (basis j))
-      ((SchwartzMap.fderivCLM ℂ (Space d) ℂ) g)
-  have hstar_fderiv : ∀ x : Space d,
-      (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x =
-      fderiv ℝ (fun y => star (f y)) x (basis i) * f' x := by
-    intro x; congr 1
-    change star (fderiv ℝ (⇑f) x (basis i)) = _
+    (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x = (Complex.I * ↑↑ℏ) *
+    ((starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x) from fun x => by ring,
+    show ∀ x : Space d, (starRingEnd ℂ) (f x) *
+    (Complex.I * ↑↑ℏ * Space.deriv i (⇑f') x) = (Complex.I * ↑↑ℏ) *
+    ((starRingEnd ℂ) (f x) * Space.deriv i (⇑f') x) from fun x => by ring]
+  rw [integral_const_mul, integral_const_mul, neg_mul_eq_mul_neg]; congr 1
+  let dS (g : 𝓢(Space d, ℂ)) :=
+    (SchwartzMap.evalCLM ℂ _ ℂ (basis i)) ((SchwartzMap.fderivCLM ℂ _ ℂ) g)
+  have hsd : ∀ x, (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x =
+      fderiv ℝ (fun y => star (f y)) x (basis i) * f' x := fun x => by
+    congr 1; change star (fderiv ℝ (⇑f) x (basis i)) = _
     rw [fderiv_star (𝕜 := ℝ)]; simp
-  simp_rw [hstar_fderiv]
-  change ∫ x, fderiv ℝ (fun y => star (f y)) x (basis i) *
-    f' x = -(∫ x, star (f x) *
-    fderiv ℝ (⇑f') x (basis i))
+  simp_rw [hsd]
+  change ∫ x, fderiv ℝ (fun y => star (f y)) x (basis i) * f' x =
+    -(∫ x, star (f x) * fderiv ℝ (⇑f') x (basis i))
   have ibp := integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable
-    (f := fun x => star (f x)) (g := ⇑f') (v := basis i)
-    (μ := volume) (hf'g := ?_) (hfg' := ?_) (hfg := ?_)
-    (Differentiable.star (SchwartzMap.differentiable f))
-    (SchwartzMap.differentiable f')
+    (f := fun x => star (f x)) (g := ⇑f') (v := basis i) (μ := volume)
+    (hf'g := ?_) (hfg' := ?_) (hfg := ?_)
+    (.star (SchwartzMap.differentiable f)) (SchwartzMap.differentiable f')
   · rw [ibp, neg_neg]
-  · have h : ∀ x, (fderiv ℝ (fun x => star (f x)) x)
-        (basis i) = star ((derivS i f) x) := by
-      intro x; rw [fderiv_star (𝕜 := ℝ)]; simp [derivS]
-    simp_rw [h]
-    exact Integrable.mul_of_top_left
-      ((ContinuousLinearEquiv.integrable_comp_iff
-        (starL' ℝ : ℂ ≃L[ℝ] ℂ)).mpr
-        (SchwartzMap.integrable (derivS i f)))
+  · have h : ∀ x, (fderiv ℝ (fun x => star (f x)) x) (basis i) =
+        star ((dS f) x) := fun x => by
+      rw [fderiv_star (𝕜 := ℝ)]; simp [dS]
+    simp_rw [h]; exact .mul_of_top_left
+      (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr (SchwartzMap.integrable _))
       (SchwartzMap.memLp_top f' volume)
-  · have h : ∀ x, (fderiv ℝ (⇑f') x) (basis i) =
-        (derivS i f') x := fun _ => rfl
-    simp_rw [h]
-    exact Integrable.mul_of_top_left
-      ((ContinuousLinearEquiv.integrable_comp_iff
-        (starL' ℝ : ℂ ≃L[ℝ] ℂ)).mpr
-        (SchwartzMap.integrable f))
-      (SchwartzMap.memLp_top (derivS i f') volume)
-  · exact Integrable.mul_of_top_left
-      ((ContinuousLinearEquiv.integrable_comp_iff
-        (starL' ℝ : ℂ ≃L[ℝ] ℂ)).mpr
-        (SchwartzMap.integrable f))
+  · have h : ∀ x, (fderiv ℝ (⇑f') x) (basis i) = (dS f') x := fun _ => rfl
+    simp_rw [h]; exact .mul_of_top_left
+      (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr (SchwartzMap.integrable f))
+      (SchwartzMap.memLp_top _ volume)
+  · exact .mul_of_top_left
+      (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr (SchwartzMap.integrable f))
       (SchwartzMap.memLp_top f' volume)
 
 /-- The symmetric momentum unbounded operators with domain the Schwartz

From 747d1d6e56f943652a5234b0dbf8bde001938f90 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 19 Mar 2026 20:49:03 +0100
Subject: [PATCH 4/7] golf(Momentum): fold unfold and integral_neg into simp
 only

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
---
 .../DDimensions/Operators/Momentum.lean                | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
index fcc70947c..8ecd59cdb 100644
--- a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -109,12 +109,10 @@ lemma momentumOperatorSchwartz_isSymmetric :
   intro ψ ψ'
   obtain ⟨f, rfl⟩ := schwartzEquiv.surjective ψ
   obtain ⟨f', rfl⟩ := schwartzEquiv.surjective ψ'
-  unfold momentumOperatorSchwartz
-  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, ContinuousLinearMap.coe_coe,
-    Function.comp_apply, LinearEquiv.symm_apply_apply, schwartzEquiv_inner,
-    momentumOperator_apply, neg_mul, map_neg, map_mul, Complex.conj_I,
-    Complex.conj_ofReal, neg_neg, mul_neg]
-  rw [integral_neg]
+  simp only [momentumOperatorSchwartz, LinearMap.coe_comp, LinearEquiv.coe_coe,
+    ContinuousLinearMap.coe_coe, Function.comp_apply, LinearEquiv.symm_apply_apply,
+    schwartzEquiv_inner, momentumOperator_apply, neg_mul, map_neg, map_mul, Complex.conj_I,
+    Complex.conj_ofReal, neg_neg, mul_neg, integral_neg]
   simp_rw [show ∀ x : Space d, Complex.I * ↑↑ℏ *
     (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x = (Complex.I * ↑↑ℏ) *
     ((starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x) from fun x => by ring,

From 2fa45ad20477ccd550b51fdad93d7a80e9caf55c Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 20 Mar 2026 14:54:21 +0000
Subject: [PATCH 5/7] 10 line golf

---
 .../DDimensions/Operators/Momentum.lean       | 33 +++++++------------
 1 file changed, 12 insertions(+), 21 deletions(-)

diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
index 8ecd59cdb..6fc49c83b 100644
--- a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -113,35 +113,26 @@ lemma momentumOperatorSchwartz_isSymmetric :
     ContinuousLinearMap.coe_coe, Function.comp_apply, LinearEquiv.symm_apply_apply,
     schwartzEquiv_inner, momentumOperator_apply, neg_mul, map_neg, map_mul, Complex.conj_I,
     Complex.conj_ofReal, neg_neg, mul_neg, integral_neg]
-  simp_rw [show ∀ x : Space d, Complex.I * ↑↑ℏ *
-    (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x = (Complex.I * ↑↑ℏ) *
-    ((starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x) from fun x => by ring,
-    show ∀ x : Space d, (starRingEnd ℂ) (f x) *
-    (Complex.I * ↑↑ℏ * Space.deriv i (⇑f') x) = (Complex.I * ↑↑ℏ) *
-    ((starRingEnd ℂ) (f x) * Space.deriv i (⇑f') x) from fun x => by ring]
-  rw [integral_const_mul, integral_const_mul, neg_mul_eq_mul_neg]; congr 1
+  field_simp
+  simp only [Space.deriv_eq, mul_assoc, integral_const_mul, neg_mul_eq_mul_neg, ]
+  congr 2
   let dS (g : 𝓢(Space d, ℂ)) :=
     (SchwartzMap.evalCLM ℂ _ ℂ (basis i)) ((SchwartzMap.fderivCLM ℂ _ ℂ) g)
-  have hsd : ∀ x, (starRingEnd ℂ) (Space.deriv i (⇑f) x) * f' x =
-      fderiv ℝ (fun y => star (f y)) x (basis i) * f' x := fun x => by
-    congr 1; change star (fderiv ℝ (⇑f) x (basis i)) = _
-    rw [fderiv_star (𝕜 := ℝ)]; simp
-  simp_rw [hsd]
-  change ∫ x, fderiv ℝ (fun y => star (f y)) x (basis i) * f' x =
-    -(∫ x, star (f x) * fderiv ℝ (⇑f') x (basis i))
-  have ibp := integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable
-    (f := fun x => star (f x)) (g := ⇑f') (v := basis i) (μ := volume)
-    (hf'g := ?_) (hfg' := ?_) (hfg := ?_)
-    (.star (SchwartzMap.differentiable f)) (SchwartzMap.differentiable f')
-  · rw [ibp, neg_neg]
+  simp only [starRingEnd_apply]
+  rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable _ _ _
+    (.star (SchwartzMap.differentiable f))  (SchwartzMap.differentiable f'), neg_neg]
+  · simp only [fderiv_star]
+    rfl
   · have h : ∀ x, (fderiv ℝ (fun x => star (f x)) x) (basis i) =
         star ((dS f) x) := fun x => by
       rw [fderiv_star (𝕜 := ℝ)]; simp [dS]
-    simp_rw [h]; exact .mul_of_top_left
+    simp_rw [h]
+    exact .mul_of_top_left
       (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr (SchwartzMap.integrable _))
       (SchwartzMap.memLp_top f' volume)
   · have h : ∀ x, (fderiv ℝ (⇑f') x) (basis i) = (dS f') x := fun _ => rfl
-    simp_rw [h]; exact .mul_of_top_left
+    simp_rw [h]
+    exact .mul_of_top_left
       (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr (SchwartzMap.integrable f))
       (SchwartzMap.memLp_top _ volume)
   · exact .mul_of_top_left

From 8dcbc7bb9ae804d481dce10d2dc6a93cf747d529 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 20 Mar 2026 15:03:50 +0000
Subject: [PATCH 6/7] refactor: further golf

---
 .../DDimensions/Operators/Momentum.lean       | 27 +++++++------------
 1 file changed, 9 insertions(+), 18 deletions(-)

diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
index 6fc49c83b..b9a33f337 100644
--- a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -114,30 +114,21 @@ lemma momentumOperatorSchwartz_isSymmetric :
     schwartzEquiv_inner, momentumOperator_apply, neg_mul, map_neg, map_mul, Complex.conj_I,
     Complex.conj_ofReal, neg_neg, mul_neg, integral_neg]
   field_simp
-  simp only [Space.deriv_eq, mul_assoc, integral_const_mul, neg_mul_eq_mul_neg, ]
+  simp only [Space.deriv_eq, mul_assoc, integral_const_mul, neg_mul_eq_mul_neg]
   congr 2
-  let dS (g : 𝓢(Space d, ℂ)) :=
-    (SchwartzMap.evalCLM ℂ _ ℂ (basis i)) ((SchwartzMap.fderivCLM ℂ _ ℂ) g)
   simp only [starRingEnd_apply]
   rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable _ _ _
-    (.star (SchwartzMap.differentiable f))  (SchwartzMap.differentiable f'), neg_neg]
+    (.star f.differentiable) f'.differentiable, neg_neg]
   · simp only [fderiv_star]
     rfl
-  · have h : ∀ x, (fderiv ℝ (fun x => star (f x)) x) (basis i) =
-        star ((dS f) x) := fun x => by
-      rw [fderiv_star (𝕜 := ℝ)]; simp [dS]
-    simp_rw [h]
-    exact .mul_of_top_left
-      (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr (SchwartzMap.integrable _))
-      (SchwartzMap.memLp_top f' volume)
-  · have h : ∀ x, (fderiv ℝ (⇑f') x) (basis i) = (dS f') x := fun _ => rfl
-    simp_rw [h]
-    exact .mul_of_top_left
-      (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr (SchwartzMap.integrable f))
-      (SchwartzMap.memLp_top _ volume)
-  · exact .mul_of_top_left
-      (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr (SchwartzMap.integrable f))
+  · simp only [fderiv_star]
+    exact .mul_of_top_left (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr
+        ((f.fderivCLM ℂ _ ℂ).evalCLM ℂ _ ℂ (basis i)).integrable)
       (SchwartzMap.memLp_top f' volume)
+  · exact .mul_of_top_left (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr f.integrable)
+      (((f'.fderivCLM ℂ _ ℂ).evalCLM ℂ _ ℂ (basis i)).memLp_top volume)
+  · exact .mul_of_top_left (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr f.integrable)
+      (f'.memLp_top volume)
 
 /-- The symmetric momentum unbounded operators with domain the Schwartz
   submodule of the Hilbert space. -/

From 79e86302ea7df6debc70b177301ea61753bdc336 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 20 Mar 2026 15:08:07 +0000
Subject: [PATCH 7/7] refactor: golf

---
 .../QuantumMechanics/DDimensions/Operators/Momentum.lean  | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
index b9a33f337..68e716551 100644
--- a/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -114,12 +114,10 @@ lemma momentumOperatorSchwartz_isSymmetric :
     schwartzEquiv_inner, momentumOperator_apply, neg_mul, map_neg, map_mul, Complex.conj_I,
     Complex.conj_ofReal, neg_neg, mul_neg, integral_neg]
   field_simp
-  simp only [Space.deriv_eq, mul_assoc, integral_const_mul, neg_mul_eq_mul_neg]
+  simp only [Space.deriv_eq, mul_assoc, integral_const_mul, neg_mul_eq_mul_neg, starRingEnd_apply]
   congr 2
-  simp only [starRingEnd_apply]
-  rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable _ _ _
-    (.star f.differentiable) f'.differentiable, neg_neg]
-  · simp only [fderiv_star]
+  rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable _ _ _ (by fun_prop) (by fun_prop)]
+  · simp only [neg_neg, fderiv_star]
     rfl
   · simp only [fderiv_star]
     exact .mul_of_top_left (((starL' ℝ : ℂ ≃L[ℝ] ℂ).integrable_comp_iff).mpr