From 23c4af5599717cc138414f58206a12e438de1941 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 13:40:51 +0900
Subject: [PATCH 01/12] move tendsto lemma

---
 .../DDimensions/SpaceDHilbertSpace/Basic.lean  | 18 ++++++++++++++++++
 .../PolyBddSchwartzSubmodule.lean              | 11 -----------
 2 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
index cfd72cfcc..fab89cf45 100644
--- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
+++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
@@ -152,6 +152,24 @@ lemma mk_eq_iff {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} :
 lemma ext_iff {f g : SpaceDHilbertSpace d} :
     f = g ↔ (f : Space d → ℂ) =ᵐ[volume] (g : Space d → ℂ) := Lp.ext_iff
 
+
+/-!
+## Limits
+-/
+
+open Filter
+
+lemma tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq
+    {d : ℕ} {α : Type*} {l : Filter α} {ψ : α → SpaceDHilbertSpace d} :
+    Tendsto ψ l (nhds 0) ↔ Tendsto (fun a ↦ ∫⁻ x : Space d, ‖ψ a x‖ₑ ^ 2) l (nhds 0) := by
+  trans Tendsto (fun a ↦ (∫⁻ x, ‖ψ a x‖ₑ ^ 2) ^ (2⁻¹ : ℝ)) l (nhds 0)
+  · simp [tendsto_iff_edist_tendsto_0, edist_zero_right, Lp.enorm_def, eLpNorm, eLpNorm']
+  constructor <;> intro h
+  · apply Tendsto.ennrpow_const 2 at h
+    simp_all [← ENNReal.rpow_mul_natCast]
+  · apply Tendsto.ennrpow_const 2⁻¹ at h
+    simp_all
+
 end SpaceDHilbertSpace
 end
 end QuantumMechanics
diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
index 649244bf7..fd40d36b2 100644
--- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
@@ -144,17 +144,6 @@ private lemma enorm_bump_mul_le_enorm {𝕜 E : Type*} [RCLike 𝕜] [NormedAddC
   rw [norm_algebraMap', Real.norm_eq_abs, norm_one, ← abs_one]
   exact abs_le_abs_of_nonneg f.nonneg f.le_one
 
-private lemma tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq
-    {d : ℕ} {α : Type*} {l : Filter α} {ψ : α → SpaceDHilbertSpace d} :
-    Tendsto ψ l (nhds 0) ↔ Tendsto (fun a ↦ ∫⁻ x : Space d, ‖ψ a x‖ₑ ^ 2) l (nhds 0) := by
-  trans Tendsto (fun a ↦ (∫⁻ x, ‖ψ a x‖ₑ ^ 2) ^ (2⁻¹ : ℝ)) l (nhds 0)
-  · simp [tendsto_iff_edist_tendsto_0, edist_zero_right, Lp.enorm_def, eLpNorm, eLpNorm']
-  constructor <;> intro h
-  · apply Tendsto.ennrpow_const 2 at h
-    simp_all [← ENNReal.rpow_mul_natCast]
-  · apply Tendsto.ennrpow_const 2⁻¹ at h
-    simp_all
-
 private lemma polyBddSchwartzSubmodule_zero_top_dense :
     Dense (polyBddSchwartzSubmodule 0 ⊤ : Set (SpaceDHilbertSpace 0)) := by
   suffices polyBddSchwartzMap 0 ⊤ = ⊤ by

From 0747d819c0e8cf1a54dd69746333e174235c3cd4 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 13:41:55 +0900
Subject: [PATCH 02/12] schwartz

---
 .../SpaceDHilbertSpace/SchwartzSubmodule.lean | 50 +++++++++++--------
 1 file changed, 30 insertions(+), 20 deletions(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean
index bc5c13b57..389f6a12f 100644
--- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean
@@ -22,6 +22,10 @@ In this module we define the Schwartz submodule of `SpaceDHilbertSpace`.
 
 ## iii. Table of contents
 
+- A. Definitions
+- B. Coercions
+- D. Misc.
+
 ## iv. References
 
 -/
@@ -31,18 +35,18 @@ In this module we define the Schwartz submodule of `SpaceDHilbertSpace`.
 namespace QuantumMechanics
 namespace SpaceDHilbertSpace
 
+noncomputable section
+
 open MeasureTheory
 open InnerProductSpace
 open SchwartzMap
 
+variable {d : ℕ}
+
 /-!
-## A. Schwartz submodule
+## A. Definitions
 -/
 
-noncomputable section
-
-variable {d : ℕ}
-
 set_option backward.isDefEq.respectTransparency false in
 /-- The continuous linear map including Schwartz maps into `SpaceDHilbertSpace d`. -/
 def schwartzIncl : 𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d := toLpCLM ℂ (E := Space d) ℂ 2
@@ -51,30 +55,39 @@ set_option backward.isDefEq.respectTransparency false in
 /-- The submodule of `SpaceDHilbertSpace d` corresponding to Schwartz maps. -/
 abbrev schwartzSubmodule (d : ℕ) := (schwartzIncl (d := d)).range
 
-instance : CoeFun (schwartzSubmodule d) fun _ ↦ Space d → ℂ := ⟨fun ψ ↦ ψ.val⟩
-
-@[simp]
-lemma val_eq_coe (ψ : schwartzSubmodule d) (x : Space d) : ψ.val x = ψ x := rfl
-
-lemma schwartzSubmodule_dense (d : ℕ) :
-    Dense (schwartzSubmodule d : Set (SpaceDHilbertSpace d)) :=
-  denseRange_toLpCLM ENNReal.top_ne_ofNat.symm
-
 set_option backward.isDefEq.respectTransparency false in
 /-- The linear equivalence between the Schwartz maps `𝓢(Space d, ℂ)` and the Schwartz submodule
   of `SpaceDHilbertSpace d`. -/
 def schwartzEquiv : 𝓢(Space d, ℂ) ≃ₗ[ℂ] schwartzSubmodule d :=
   LinearEquiv.ofInjective schwartzIncl.toLinearMap (injective_toLp (E := Space d) 2)
 
+namespace SchwartzSubmodule
+
 variable (f g : 𝓢(Space d, ℂ)) (ψ : schwartzSubmodule d)
 
-lemma schwartzEquiv_coe_ae : (schwartzEquiv f) =ᵐ[volume] f := coeFn_toLp f 2 volume
+/-!
+## B. Coercions
+-/
+
+instance : CoeFun (schwartzSubmodule d) fun _ ↦ Space d → ℂ := ⟨fun ψ ↦ ψ.val⟩
+
+lemma schwartzEquiv_apply_coe : ↑(schwartzEquiv f) = schwartzIncl f := by simp [schwartzEquiv]
+
+lemma schwartzEquiv_coe_ae : schwartzEquiv f =ᵐ[volume] f := coeFn_toLp f 2 volume
 
 lemma schwartzEquiv_symm_coe_ae : schwartzEquiv.symm ψ =ᵐ[volume] ψ := by
   nth_rw 2 [← schwartzEquiv.apply_symm_apply ψ]
   exact (schwartzEquiv_coe_ae _).symm
 
-lemma schwartzEquiv_apply_coe : ↑(schwartzEquiv f) = schwartzIncl f := by simp [schwartzEquiv]
+lemma schwartzEquiv_ae_eq (h : schwartzEquiv f =ᵐ[volume] schwartzEquiv g) : f = g :=
+  (EmbeddingLike.apply_eq_iff_eq _).mp (SetLike.coe_eq_coe.mp (ext_iff.mpr h))
+
+/-!
+## C. Misc.
+-/
+
+lemma dense (d : ℕ) : Dense (schwartzSubmodule d : Set (SpaceDHilbertSpace d)) :=
+  denseRange_toLpCLM ENNReal.top_ne_ofNat.symm
 
 lemma schwartzEquiv_inner :
     ⟪schwartzEquiv f, schwartzEquiv g⟫_ℂ = ∫ x : Space d, starRingEnd ℂ (f x) * g x := by
@@ -82,13 +95,10 @@ lemma schwartzEquiv_inner :
   filter_upwards [schwartzEquiv_coe_ae f, schwartzEquiv_coe_ae g] with _ hf hg
   simp [hf, hg, mul_comm]
 
-lemma schwartzEquiv_ae_eq (h : schwartzEquiv f =ᵐ[volume] schwartzEquiv g) : f = g :=
-  (EmbeddingLike.apply_eq_iff_eq _).mp (SetLike.coe_eq_coe.mp (ext_iff.mpr h))
-
 lemma schwartzIncl_ker : schwartzIncl.ker = (⊥ : Submodule ℂ 𝓢(Space d, ℂ)) := by
   ext; simp [← schwartzEquiv_apply_coe]
 
+end SchwartzSubmodule
 end
-
 end SpaceDHilbertSpace
 end QuantumMechanics

From ee5e000185d8c5977a3951e9bd68ae577366e05d Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 13:45:07 +0900
Subject: [PATCH 03/12] polybdd coercions

---
 .../PolyBddSchwartzSubmodule.lean             | 29 ++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
index fd40d36b2..ec1abe246 100644
--- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
@@ -105,7 +105,34 @@ def polyBddSchwartzEquiv {d : ℕ} {a : ℕ∞} :
   LinearEquiv.ofInjective polyBddSchwartzIncl.toLinearMap (polyBddSchwartzIncl_injective d a)
 
 /-!
-### B. (In)equalities
+## B. Coercions
+-/
+
+instance {d : ℕ} {a : ℕ∞} : CoeOut (polyBddSchwartzMap d a) 𝓢(Space d, ℂ) := ⟨fun f ↦ f.val⟩
+
+instance {d : ℕ} {a : ℕ∞} : CoeFun (polyBddSchwartzMap d a) (fun _ ↦ Space d → ℂ) :=
+  ⟨fun f ↦ ⇑f.val⟩
+
+@[simp]
+lemma toFun_eq_coe {d : ℕ} {a : ℕ∞} (f : polyBddSchwartzMap d a) (x : Space d) :
+    f.val.toFun x = f.val x :=
+  rfl
+
+lemma polyBddSchwartzEquiv_symm_apply_coe {d : ℕ} {a : ℕ∞}
+    {ψ : schwartzSubmodule d} (hψ : ↑ψ ∈ polyBddSchwartzSubmodule d a) :
+    (polyBddSchwartzEquiv.symm ⟨ψ, hψ⟩).val = schwartzEquiv.symm ψ := by
+  apply schwartzEquiv.injective
+  apply SetLike.coe_eq_coe.mp
+  obtain ⟨g, hg⟩ := polyBddSchwartzEquiv.surjective ⟨ψ.val, hψ⟩
+  have hg' : polyBddSchwartzIncl g = ψ := SetLike.coe_eq_coe.mpr hg
+  rw [← hg, LinearEquiv.symm_apply_apply, LinearEquiv.apply_symm_apply, ← hg']
+  rfl
+
+lemma polyBddSchwartzEquiv_coe_ae {d : ℕ} {a : ℕ∞} (f : polyBddSchwartzMap d a) :
+    polyBddSchwartzEquiv f =ᵐ[volume] f.val := schwartzEquiv_coe_ae f.val
+
+/-!
+### C. (In)equalities
 -/
 
 lemma polyBddSchwartzMap_zero_eq_top (d : ℕ) : polyBddSchwartzMap d 0 = ⊤ := by

From 2bfaa300a2619b21a0389463794177c16ee6fd7a Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 13:45:36 +0900
Subject: [PATCH 04/12] polybdd namespace

---
 .../PolyBddSchwartzSubmodule.lean             | 44 ++++++++++---------
 1 file changed, 24 insertions(+), 20 deletions(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
index ec1abe246..ef024a88a 100644
--- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
@@ -38,13 +38,14 @@ their being dense in `SpaceDHilbertSpace 0 ≅ ℂ`).
 
 - `polyBddSchwartzSubmodule d (a : ℕ∞)`: Restriction of `schwartzSubmodule d` to those Schwartz maps
   which are bounded by powers of `‖x‖`.
-- `polyBddSchwartzSubmodule_dense d a`: These submodules are dense in `SpaceDHilbertSpace`.
+- `PolyBddSchwartzSubmodule.dense d a`: These submodules are dense in `SpaceDHilbertSpace`.
 
 ## iii. Table of contents
 
 - A. Definitions
-- B. (In)equalities
-- C. Density
+- B. Coercions
+- C. (In)equalities
+- D. Density
 
 ## iv. References
 
@@ -55,14 +56,15 @@ their being dense in `SpaceDHilbertSpace 0 ≅ ℂ`).
 namespace QuantumMechanics
 namespace SpaceDHilbertSpace
 
+noncomputable section
+
 open MeasureTheory
 open InnerProductSpace
 open SchwartzMap
-
-noncomputable section
+open SchwartzSubmodule
 
 /-!
-### A. Definitions
+## A. Definitions
 -/
 
 /-- A function is a bounded Schwartz map if it is both Schwartz and bounded by powers of `‖x‖`. -/
@@ -104,6 +106,8 @@ def polyBddSchwartzEquiv {d : ℕ} {a : ℕ∞} :
     polyBddSchwartzMap d a ≃ₗ[ℂ] polyBddSchwartzSubmodule d a :=
   LinearEquiv.ofInjective polyBddSchwartzIncl.toLinearMap (polyBddSchwartzIncl_injective d a)
 
+namespace PolyBddSchwartzSubmodule
+
 /-!
 ## B. Coercions
 -/
@@ -140,23 +144,23 @@ lemma polyBddSchwartzMap_zero_eq_top (d : ℕ) : polyBddSchwartzMap d 0 = ⊤ :=
   have := f.decay 0 0
   simp_all [polyBddSchwartzMap]
 
-lemma polyBddSchwartzMap_le_of_ge (d : ℕ) {a b : ℕ∞} (h : a ≤ b) :
+lemma polyBddSchwartzMap_antitone (d : ℕ) {a b : ℕ∞} (h : a ≤ b) :
     polyBddSchwartzMap d b ≤ polyBddSchwartzMap d a := fun _ hx k hk ↦ hx k (hk.trans h)
 
-lemma polyBddSchwartzSubmodule_zero_eq (d : ℕ) :
+lemma of_zero_eq (d : ℕ) :
     polyBddSchwartzSubmodule d 0 = schwartzSubmodule d := by
   simp [polyBddSchwartzSubmodule, polyBddSchwartzIncl, polyBddSchwartzMap_zero_eq_top]
 
-lemma polyBddSchwartzSubmodule_le (d : ℕ) (a : ℕ∞) :
+lemma le_schwartzSubmodule (d : ℕ) (a : ℕ∞) :
     polyBddSchwartzSubmodule d a ≤ schwartzSubmodule d := LinearMap.range_domRestrict_le_range _ _
 
-lemma polyBddSchwartzSubmodule_le_of_ge (d : ℕ) {a b : ℕ∞} (h : a ≤ b) :
+lemma antitone (d : ℕ) {a b : ℕ∞} (h : a ≤ b) :
     polyBddSchwartzSubmodule d b ≤ polyBddSchwartzSubmodule d a := by
   simp only [polyBddSchwartzSubmodule, polyBddSchwartzIncl, LinearMap.range_domRestrict]
-  exact Submodule.map_mono (polyBddSchwartzMap_le_of_ge d h)
+  exact Submodule.map_mono (polyBddSchwartzMap_antitone d h)
 
 /-!
-### C. Density
+### D. Density
 -/
 
 open Filter Complex
@@ -171,10 +175,10 @@ private lemma enorm_bump_mul_le_enorm {𝕜 E : Type*} [RCLike 𝕜] [NormedAddC
   rw [norm_algebraMap', Real.norm_eq_abs, norm_one, ← abs_one]
   exact abs_le_abs_of_nonneg f.nonneg f.le_one
 
-private lemma polyBddSchwartzSubmodule_zero_top_dense :
+private lemma dense_zero_top :
     Dense (polyBddSchwartzSubmodule 0 ⊤ : Set (SpaceDHilbertSpace 0)) := by
   suffices polyBddSchwartzMap 0 ⊤ = ⊤ by
-    simp [polyBddSchwartzSubmodule, polyBddSchwartzIncl, this, schwartzSubmodule_dense]
+    simp [polyBddSchwartzSubmodule, polyBddSchwartzIncl, this, SchwartzSubmodule.dense]
   refine Submodule.eq_top_iff'.mpr (fun f k hk ↦ ?_)
   refine ⟨1 + ‖f 0‖, by positivity, fun x ↦ ?_⟩
   simp only [Space.point_dim_zero_eq, norm_zero, zpow_neg, zpow_natCast]
@@ -182,16 +186,16 @@ private lemma polyBddSchwartzSubmodule_zero_top_dense :
   · simp
   · simp [hk', add_nonneg]
 
-lemma polyBddSchwartzSubmodule_top_dense (d : ℕ) :
+lemma dense_top (d : ℕ) :
     Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDHilbertSpace d)) := by
   rcases eq_zero_or_pos d with (rfl | hd)
   · -- `d = 0`: Every function `Space 0 ≅ {0} → ℂ` is in `polyBddSchwartzSubmodule 0 ⊤`.
-    exact polyBddSchwartzSubmodule_zero_top_dense
+    exact dense_zero_top
   · -- `d > 0`: Construct a sequence in `polyBddSchwartzSubmodule d ⊤` which tends to `ξ`
     intro ξ
     apply mem_closure_iff_seq_limit.mpr
     -- `ψₙ = [fₙ]` is a sequence in `schwartzSubmodule` which tends to `ξ`
-    obtain ⟨ψ, hψ, hψξ⟩ := mem_closure_iff_seq_limit.mp (schwartzSubmodule_dense d ξ)
+    obtain ⟨ψ, hψ, hψξ⟩ := mem_closure_iff_seq_limit.mp (SchwartzSubmodule.dense d ξ)
     let f (n : ℕ) : 𝓢(Space d, ℂ) := schwartzEquiv.symm ⟨ψ n, hψ n⟩
     -- `bₙ` is a sequence of bump functions with shrinking domain
     let b (n : ℕ) : ContDiffBump (0 : Space d) :=
@@ -284,11 +288,11 @@ lemma polyBddSchwartzSubmodule_top_dense (d : ℕ) :
         simp_rw [h, h', Pi.sub_apply, hg, s, ← mul_sub]
         exact ENNReal.pow_le_pow_left <| enorm_bump_mul_le_enorm (b n) (fun x ↦ f n x - ξ x) x
 
-lemma polyBddSchwartzSubmodule_dense (d : ℕ) (a : ℕ∞) :
+lemma dense (d : ℕ) (a : ℕ∞) :
     Dense (polyBddSchwartzSubmodule d a : Set (SpaceDHilbertSpace d)) :=
-  (polyBddSchwartzSubmodule_top_dense d).mono (polyBddSchwartzSubmodule_le_of_ge d le_top)
+  (dense_top d).mono (antitone d le_top)
 
+end PolyBddSchwartzSubmodule
 end
-
 end SpaceDHilbertSpace
 end QuantumMechanics

From 1e51e71bd4fb3b61ebade00b3cc7220bb4b8bbcd Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 13:53:25 +0900
Subject: [PATCH 05/12] fixes

---
 .../QuantumMechanics/DDimensions/Operators/Momentum.lean    | 6 ++++--
 .../QuantumMechanics/DDimensions/Operators/Position.lean    | 5 +++--
 .../DDimensions/SpaceDHilbertSpace/Basic.lean               | 1 -
 3 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean
index 27a32c1cf..4c081db78 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -79,7 +79,9 @@ lemma momentumOperator_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) : 𝐩 i ψ
 
 -/
 
-open SpaceDHilbertSpace MeasureTheory
+open MeasureTheory
+open SpaceDHilbertSpace
+open SchwartzSubmodule
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The momentum operators defined on the Schwartz submodule. -/
@@ -115,7 +117,7 @@ lemma momentumOperatorSchwartz_isSymmetric :
   submodule of the Hilbert space. -/
 def momentumUnboundedOperator :
     UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
-  UnboundedOperator.ofSymmetric (schwartzSubmodule_dense d)
+  UnboundedOperator.ofSymmetric (SchwartzSubmodule.dense d)
     (momentumOperatorSchwartz_isSymmetric i)
 
 end
diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
index 82a4ee08e..4fcb337ad 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
@@ -364,6 +364,7 @@ end
 noncomputable section
 
 open SpaceDHilbertSpace
+open SchwartzSubmodule
 
 /-!
 ### B.1. Position vector
@@ -389,7 +390,7 @@ lemma positionOperatorSchwartz_isSymmetric : (positionOperatorSchwartz i).IsSymm
 /-- The symmetric position unbounded operators with domain the Schwartz submodule
   of the Hilbert space. -/
 def positionUnboundedOperator : UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
-  UnboundedOperator.ofSymmetric (schwartzSubmodule_dense d) (positionOperatorSchwartz_isSymmetric i)
+  UnboundedOperator.ofSymmetric (SchwartzSubmodule.dense d) (positionOperatorSchwartz_isSymmetric i)
 
 /-!
 ### B.2. Radius powers (regularized)
@@ -418,7 +419,7 @@ lemma radiusRegPowOperatorSchwartz_isSymmetric {d : ℕ} (ε : ℝˣ) (s : ℝ)
   of the Hilbert space. -/
 def radiusRegPowUnboundedOperator {d : ℕ} (ε : ℝˣ) (s : ℝ) :
     UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
-  UnboundedOperator.ofSymmetric (schwartzSubmodule_dense d)
+  UnboundedOperator.ofSymmetric (SchwartzSubmodule.dense d)
     (radiusRegPowOperatorSchwartz_isSymmetric ε s)
 
 end
diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
index fab89cf45..5cca12031 100644
--- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
+++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
@@ -152,7 +152,6 @@ lemma mk_eq_iff {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} :
 lemma ext_iff {f g : SpaceDHilbertSpace d} :
     f = g ↔ (f : Space d → ℂ) =ᵐ[volume] (g : Space d → ℂ) := Lp.ext_iff
 
-
 /-!
 ## Limits
 -/

From 611d926a51c3a07df4f9dbe336fad92c113f0562 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 14:25:47 +0900
Subject: [PATCH 06/12] ofSymmetric variant

---
 .../DDimensions/Operators/Momentum.lean       |  4 +--
 .../DDimensions/Operators/Position.lean       |  6 ++---
 .../DDimensions/Operators/Unbounded.lean      | 25 ++++++++++++-------
 3 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean
index 4c081db78..83bd03922 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean
@@ -82,6 +82,7 @@ lemma momentumOperator_apply (ψ : 𝓢(Space d, ℂ)) (x : Space d) : 𝐩 i ψ
 open MeasureTheory
 open SpaceDHilbertSpace
 open SchwartzSubmodule
+open UnboundedOperator
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The momentum operators defined on the Schwartz submodule. -/
@@ -117,8 +118,7 @@ lemma momentumOperatorSchwartz_isSymmetric :
   submodule of the Hilbert space. -/
 def momentumUnboundedOperator :
     UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
-  UnboundedOperator.ofSymmetric (SchwartzSubmodule.dense d)
-    (momentumOperatorSchwartz_isSymmetric i)
+  ofSymmetric' (SchwartzSubmodule.dense d) (momentumOperatorSchwartz_isSymmetric i)
 
 end
 end QuantumMechanics
diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
index 4fcb337ad..2c358aff9 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
@@ -365,6 +365,7 @@ noncomputable section
 
 open SpaceDHilbertSpace
 open SchwartzSubmodule
+open UnboundedOperator
 
 /-!
 ### B.1. Position vector
@@ -390,7 +391,7 @@ lemma positionOperatorSchwartz_isSymmetric : (positionOperatorSchwartz i).IsSymm
 /-- The symmetric position unbounded operators with domain the Schwartz submodule
   of the Hilbert space. -/
 def positionUnboundedOperator : UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
-  UnboundedOperator.ofSymmetric (SchwartzSubmodule.dense d) (positionOperatorSchwartz_isSymmetric i)
+  ofSymmetric' (SchwartzSubmodule.dense d) (positionOperatorSchwartz_isSymmetric i)
 
 /-!
 ### B.2. Radius powers (regularized)
@@ -419,8 +420,7 @@ lemma radiusRegPowOperatorSchwartz_isSymmetric {d : ℕ} (ε : ℝˣ) (s : ℝ)
   of the Hilbert space. -/
 def radiusRegPowUnboundedOperator {d : ℕ} (ε : ℝˣ) (s : ℝ) :
     UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
-  UnboundedOperator.ofSymmetric (SchwartzSubmodule.dense d)
-    (radiusRegPowOperatorSchwartz_isSymmetric ε s)
+  ofSymmetric' (SchwartzSubmodule.dense d) (radiusRegPowOperatorSchwartz_isSymmetric ε s)
 
 end
 end QuantumMechanics
diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean
index 94cf763c3..e85a0f280 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean
@@ -498,20 +498,27 @@ section
 
 variable
   {E : Submodule ℂ H} (hE : Dense (E : Set H))
-  {f : E →ₗ[ℂ] E} (hf : f.IsSymmetric)
+  {f : E →ₗ[ℂ] H} (hf : ∀ x y : E, ⟪f x, ↑y⟫_ℂ = ⟪↑x, f y⟫_ℂ)
+  {g : E →ₗ[ℂ] E} (hg : g.IsSymmetric)
   (T : UnboundedOperator H H)
 
 /-- An `UnboundedOperator` constructed from a symmetric linear map on a dense submodule `E`. -/
 def ofSymmetric : UnboundedOperator H H where
-  toLinearPMap := LinearPMap.mk E (E.subtype ∘ₗ f)
+  toLinearPMap := LinearPMap.mk E f
   dense_domain := hE
   is_closable := by
-    refine isClosable_iff_exists_closed_extension.mpr ?_
-    use (LinearPMap.mk E (E.subtype ∘ₗ f))†
-    exact ⟨LinearPMap.adjoint_isClosed hE, IsFormalAdjoint.le_adjoint hE hf⟩
+    apply isClosable_iff_exists_closed_extension.mpr
+    exact ⟨(LinearPMap.mk E f)†, LinearPMap.adjoint_isClosed hE, IsFormalAdjoint.le_adjoint hE hf⟩
+
+/-- An `UnboundedOperators` constructed from a symmetric linear map on a dense submodule `E`
+  to itself. -/
+def ofSymmetric' : UnboundedOperator H H := ofSymmetric (f := E.subtype ∘ₗ g) hE hg
+
+@[simp]
+lemma ofSymmetric_apply (ψ : E) : ofSymmetric hE hf ψ = f ψ := rfl
 
 @[simp]
-lemma ofSymmetric_apply (ψ : E) : (ofSymmetric hE hf) ψ = E.subtype (f ψ) := rfl
+lemma ofSymmetric'_apply (ψ : E) : ofSymmetric' hE hg ψ = g ψ := rfl
 
 -- Note that cannot simply co-opt `LinearMap.IsSymmetric` because
 -- the domain and codomain of `T` need not be the same.
@@ -582,7 +589,7 @@ section
 
 variable
   {E : Submodule ℂ H} (hE : Dense (E : Set H))
-  {f : E →ₗ[ℂ] E} (hf : f.IsSymmetric)
+  {g : E →ₗ[ℂ] E} (hg : g.IsSymmetric)
   (T : UnboundedOperator H H)
 
 /-- A map `F : D(T) →L[ℂ] ℂ` is a generalized eigenvector of an unbounded operator `T`
@@ -591,11 +598,11 @@ def IsGeneralizedEigenvector (F : T.domain →L[ℂ] ℂ) (c : ℂ) : Prop :=
   ∀ ψ : T.domain, ∃ ψ' : T.domain, ψ' = T ψ ∧ F ψ' = c • F ψ
 
 lemma isGeneralizedEigenvector_ofSymmetric_iff (F : E →L[ℂ] ℂ) (c : ℂ) :
-    IsGeneralizedEigenvector (ofSymmetric hE hf) F c ↔ ∀ ψ : E, F (f ψ) = c • F ψ := by
+    IsGeneralizedEigenvector (ofSymmetric' hE hg) F c ↔ ∀ ψ : E, F (g ψ) = c • F ψ := by
   constructor <;> intro h ψ
   · obtain ⟨ψ', hψ', hψ''⟩ := h ψ
     exact (SetLike.coe_eq_coe.mp hψ') ▸ hψ''
-  · use f ψ
+  · use g ψ
     exact ⟨by simp, h ψ⟩
 
 end

From 192555033924d3b30fb927c648a4781de6316b7a Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 14:39:45 +0900
Subject: [PATCH 07/12] move opens

---
 .../DDimensions/Operators/Position.lean       | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
index 2c358aff9..fec578cf3 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
@@ -6,7 +6,7 @@ Authors: Gregory J. Loges
 module
 
 public import Physlib.QuantumMechanics.DDimensions.Operators.Unbounded
-public import Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
+public import Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.PolyBddSchwartzSubmodule
 public import Physlib.SpaceAndTime.Space.Integrals.NormPow
 public import Physlib.SpaceAndTime.Space.Derivatives.Basic
 /-!
@@ -53,10 +53,14 @@ Notation:
 
 @[expose] public section
 
-open Physlib
-
 namespace QuantumMechanics
 
+open Filter
+open MeasureTheory
+open SchwartzMap
+open SpaceDHilbertSpace
+open SchwartzSubmodule PolyBddSchwartzSubmodule
+
 variable {d : ℕ} (i : Fin d)
 
 /-!
@@ -65,7 +69,6 @@ variable {d : ℕ} (i : Fin d)
 
 noncomputable section
 open Space Function
-open SchwartzMap
 
 /-!
 ### A.1. Position vector
@@ -171,9 +174,6 @@ lemma positionOperatorSqr_eq {d : ℕ} (ε : ℝˣ) :
 ### A.3. Radius powers
 -/
 
-open MeasureTheory
-open SpaceDHilbertSpace
-
 set_option backward.isDefEq.respectTransparency false in
 /-- The radius operator to power `s` is the linear map from `𝓢(Space d, ℂ)` to `Space d → ℂ` that
   maps `ψ` to `x ↦ ‖x‖ˢψ(x)` (which is 'nearly' Schwartz for general `s`). -/
@@ -285,8 +285,6 @@ lemma radiusPowOperator_apply_memHS {d : ℕ} (s : ℝ) (h : 0 < d + 2 * s) (ψ
 #### A.3.1. As limit of regularized operators
 -/
 
-open Filter
-
 /-- Neighborhoods of "0" in the non-zero reals, i.e. those sets containing `(-ε,0) ∪ (0,ε) ⊆ ℝˣ`
   for some `ε > 0`. -/
 abbrev nhdsZeroUnits : Filter ℝˣ := comap (Units.coeHom ℝ) (nhds 0)
@@ -363,9 +361,8 @@ end
 
 noncomputable section
 
-open SpaceDHilbertSpace
-open SchwartzSubmodule
 open UnboundedOperator
+open InnerProductSpace
 
 /-!
 ### B.1. Position vector

From 0e2632f2533dcd2a463ce9e686ac07daad5bdfe5 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 14:40:14 +0900
Subject: [PATCH 08/12] apply_memHS generalization

---
 .../DDimensions/Operators/Position.lean       | 40 ++++++++++++-------
 1 file changed, 26 insertions(+), 14 deletions(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
index fec578cf3..ffdf766b6 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
@@ -214,32 +214,44 @@ lemma radiusPowOperator_apply_stronglyMeasurable {d : ℕ} (s : ℝ) (ψ : 𝓢(
 
 set_option backward.isDefEq.respectTransparency false in
 /-- `x ↦ ‖x‖ˢψ(x)` is square-integrable provided `s` is not too negative. -/
-lemma radiusPowOperator_apply_memHS {d : ℕ} (s : ℝ) (h : 0 < d + 2 * s) (ψ : 𝓢(Space d, ℂ)) :
+lemma radiusPowOperator_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a : ℕ)
+    (hψ : ψ ∈ polyBddSchwartzMap d a) (h : 0 < d + 2 * (a + s)) :
     MemHS (𝐫 s ψ) := by
   rcases Nat.eq_zero_or_pos d with (rfl | hd)
   · simp only [MemHS, MemLp.of_discrete]
-  · refine (MeasureTheory.memLp_two_iff_integrable_sq_norm (by fun_prop)).mpr ⟨by fun_prop, ?_⟩
-    suffices ∫⁻ (a : Space d), ‖‖ψ a‖ ^ 2 * ‖a‖ ^ (2 * s)‖ₑ < ⊤ by
+  · have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc
+    refine (memLp_two_iff_integrable_sq_norm (by fun_prop)).mpr ⟨by fun_prop, ?_⟩
+    suffices ∫⁻ (x : Space d), ‖‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s)‖ₑ < ⊤ by
       have hInt (x : Space d) : ‖𝐫 s ψ x‖ ^ 2 = ‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s) := by
         simp [radiusPowOperator, mul_pow, mul_comm, Real.rpow_mul]
       simpa only [HasFiniteIntegral, hInt]
     rw [← lintegral_add_compl _ (measurableSet_ball (x := 0) (ε := 1)), ENNReal.add_lt_top]
     constructor
-    · -- `‖x‖ < 1`: bound `‖ψ x‖` by a constant
-      obtain ⟨C, hC_pos, hC⟩ := ψ.decay 0 0
-      simp only [pow_zero, norm_iteratedFDeriv_zero, one_mul] at hC
-      suffices hBound : ∀ x, ‖‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s)‖ₑ ≤ ‖C ^ 2‖ₑ * ‖‖x‖ ^ (2 * s)‖ₑ by
+    · -- `‖x‖ < 1`: bound `‖ψ x‖` by `‖x‖ᵃ`
+      obtain ⟨C, hC_pos, hC⟩ := hψ a (le_refl _)
+      suffices hBound : ∀ᵐ x, ‖‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s)‖ₑ ≤ ‖C ^ 2‖ₑ * ‖‖x‖ ^ (2 * (a + s))‖ₑ by
         calc
-          _ ≤ ∫⁻ (x : Space d) in (Metric.ball 0 1), ‖C ^ 2‖ₑ * ‖‖x‖ ^ (2 * s)‖ₑ :=
-            setLIntegral_mono' measurableSet_ball (fun x _ ↦ hBound x)
-          _ = ‖C ^ 2‖ₑ * ∫⁻ (x : Space d) in (Metric.ball 0 1), ‖‖x‖ ^ (2 * s)‖ₑ :=
+          _ ≤ ∫⁻ (x : Space d) in (Metric.ball 0 1), ‖C ^ 2‖ₑ * ‖‖x‖ ^ (2 * (a + s))‖ₑ :=
+            setLIntegral_mono_ae' measurableSet_ball (Eventually.mono hBound fun _ h' _ ↦ h')
+          _ = ‖C ^ 2‖ₑ * ∫⁻ (x : Space d) in (Metric.ball 0 1), ‖‖x‖ ^ (2 * (a + s))‖ₑ :=
             lintegral_const_mul _ (by fun_prop)
         apply ENNReal.mul_lt_top enorm_lt_top
         exact ((integrableOn_norm_rpow_ball_iff hd Real.zero_lt_one _).mpr h).hasFiniteIntegral
-      intro x
-      simp_rw [← enorm_mul, enorm_le_iff_norm_le, norm_mul, norm_pow, Real.norm_eq_abs, sq_abs]
-      refine mul_le_mul_of_nonneg_right ?_ (abs_nonneg _)
-      exact (sq_le_sq₀ (norm_nonneg _) hC_pos.le).mpr (hC x)
+      apply ae_iff.mpr
+      refine measure_mono_null ?_ (measure_singleton 0)
+      intro x hx
+      by_contra hx'
+      apply hx
+      apply norm_pos_iff.mpr at hx'
+      simp_rw [← enorm_mul, enorm_le_iff_norm_le, mul_add, Real.rpow_add hx', norm_mul, ← mul_assoc]
+      refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
+      simp_rw [← Nat.cast_two (R := ℝ), mul_comm, Real.rpow_mul_natCast hx'.le, norm_pow, ← mul_pow,
+        norm_norm, Real.norm_eq_abs, abs_of_pos hC_pos, abs_of_nonneg (Real.rpow_nonneg hx'.le _)]
+      apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mpr
+      apply (inv_mul_le_iff₀' (by positivity)).mp
+      rw [← Real.rpow_neg_one, ← Real.rpow_mul hx'.le, mul_comm _ (-1), neg_mul, one_mul,
+        Real.rpow_neg_natCast]
+      exact hC x
     · -- `1 ≤ ‖x‖`: bound `‖ψ x‖` by a suitable power of `‖x‖`
       obtain ⟨C, hC_pos, hC⟩ := ψ.decay (⌈s⌉.toNat + d) 0
       simp only [norm_iteratedFDeriv_zero, ← Real.rpow_natCast, Nat.cast_add] at hC

From 71ad3adebfa9e34df2968d6bf2743215dbfd1740 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 14:41:19 +0900
Subject: [PATCH 09/12] radiusPow unbounded

---
 .../DDimensions/Operators/Position.lean       | 70 +++++++++++++++++++
 1 file changed, 70 insertions(+)

diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
index ffdf766b6..3c863ed1f 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
@@ -46,6 +46,7 @@ Notation:
 - B. Unbounded operators
   - B.1. Position vector
   - B.2. Radius powers (regularized)
+  - B.3. Radius powers
 
 ## iv. References
 
@@ -185,6 +186,9 @@ def radiusPowOperator {d : ℕ} (s : ℝ) : 𝓢(Space d, ℂ) →ₗ[ℂ] Space
 @[inherit_doc radiusPowOperator]
 notation "𝐫" => radiusPowOperator
 
+@[inherit_doc radiusPowOperator]
+notation "𝐫[" d' "]" => radiusPowOperator (d := d')
+
 lemma radiusPowOperator_apply_fun {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) :
     𝐫 s ψ = fun x ↦ ‖x‖ ^ s • ψ x := rfl
 
@@ -431,5 +435,71 @@ def radiusRegPowUnboundedOperator {d : ℕ} (ε : ℝˣ) (s : ℝ) :
     UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
   ofSymmetric' (SchwartzSubmodule.dense d) (radiusRegPowOperatorSchwartz_isSymmetric ε s)
 
+@[inherit_doc radiusRegPowUnboundedOperator]
+notation "ℛ₀" => radiusRegPowUnboundedOperator
+
+@[inherit_doc radiusRegPowUnboundedOperator]
+notation "ℛ₀[" d' "]" => radiusRegPowUnboundedOperator (d := d')
+
+lemma radiusRegPowUnboundedOperator_apply_ae_eq {d : ℕ} (ε : ℝˣ) (s : ℝ) (ψ : schwartzSubmodule d) :
+    ℛ₀ ε s ψ =ᵐ[volume] 𝐫₀ ε s (schwartzEquiv.symm ψ) :=
+  schwartzEquiv_coe_ae _
+
+/-!
+### B.3. Radius powers
+-/
+
+open Complex
+
+lemma add_floor_toNat_pos_aux (d : ℕ) (s : ℝ) : 0 < d + 2 * (⌊1 - d / 2 - s⌋.toNat + s) := by
+  let n : ℤ := ⌊1 - d / 2 - s⌋
+  have hn₁ : 1 - d / 2 - s < n + 1 := Int.lt_floor_add_one _
+  have hn₂ : (n : ℝ) ≤ n.toNat := Int.cast_le.mpr (Int.self_le_toNat _)
+  linarith
+
+/-- Radius operator acting on a polynomially-bounded Schwartz submodule. -/
+def radiusPowOperatorSchwartz {d : ℕ} (s : ℝ) :
+    polyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat →ₗ[ℂ] SpaceDHilbertSpace d where
+  toFun ψ :=
+    let f := polyBddSchwartzEquiv.symm ψ
+    mk <| radiusPowOperator_apply_memHS s f.1 _ f.2 (add_floor_toNat_pos_aux d s)
+  map_add' := by simp [← mk_add]
+  map_smul' := by simp [← mk_const_smul]
+
+lemma radiusPowOperatorSchwartz_apply_ae {d : ℕ} {s : ℝ}
+    (ψ : polyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat) :
+    radiusPowOperatorSchwartz s ψ =ᵐ[volume] 𝐫 s (polyBddSchwartzEquiv.symm ψ) := by
+  let f := polyBddSchwartzEquiv.symm ψ
+  exact coe_mk_ae <| radiusPowOperator_apply_memHS s f.1 _ f.2 (add_floor_toNat_pos_aux d s)
+
+lemma radiusPowOperatorSchwartz_isSymmetric (d : ℕ) (s : ℝ) :
+    ∀ ψ φ : polyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat,
+      ⟪radiusPowOperatorSchwartz s ψ, ↑φ⟫_ℂ = ⟪↑ψ, radiusPowOperatorSchwartz s φ⟫_ℂ := by
+  intro ψ φ
+  obtain ⟨f, hf⟩ := polyBddSchwartzEquiv.surjective ψ
+  obtain ⟨g, hg⟩ := polyBddSchwartzEquiv.surjective φ
+  refine integral_congr_ae ?_
+  filter_upwards [polyBddSchwartzEquiv_coe_ae f, radiusPowOperatorSchwartz_apply_ae ψ,
+    polyBddSchwartzEquiv_coe_ae g, radiusPowOperatorSchwartz_apply_ae φ] with x h₁ h₂ h₃ h₄
+  simp_rw [h₂, h₄, ← hf, ← hg, h₁, h₃, LinearEquiv.symm_apply_apply]
+  simp only [radiusPowOperator_apply, real_smul, RCLike.inner_apply, map_mul, conj_ofReal]
+  ring
+
+/-- The symmetric radius unbounded operators with domain a polynomially-bounded Schwartz submodule
+  of the Hilbert space. -/
+def radiusPowUnboundedOperator {d : ℕ} (s : ℝ) :
+    UnboundedOperator (SpaceDHilbertSpace d) (SpaceDHilbertSpace d) :=
+  ofSymmetric (PolyBddSchwartzSubmodule.dense d _) (radiusPowOperatorSchwartz_isSymmetric d s)
+
+@[inherit_doc radiusPowUnboundedOperator]
+notation "ℛ" => radiusPowUnboundedOperator
+
+@[inherit_doc radiusPowUnboundedOperator]
+notation "ℛ[" d' "]" => radiusPowUnboundedOperator (d := d')
+
+lemma radiusPowUnboundedOperator_apply_ae {d : ℕ} (s : ℝ) (ψ : (ℛ[d] s).domain) :
+    ℛ s ψ =ᵐ[volume] 𝐫 s (polyBddSchwartzEquiv.symm ψ) :=
+  radiusPowOperatorSchwartz_apply_ae ψ
+
 end
 end QuantumMechanics

From 368191a77741f29cee1e74c05811e1447b2640ec Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sat, 2 May 2026 14:46:47 +0900
Subject: [PATCH 10/12] limit of regularized

---
 .../DDimensions/Operators/Position.lean       | 95 +++++++++++++++++++
 1 file changed, 95 insertions(+)

diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
index 3c863ed1f..4f38f34a0 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
@@ -47,6 +47,7 @@ Notation:
   - B.1. Position vector
   - B.2. Radius powers (regularized)
   - B.3. Radius powers
+    - B.3.1. As limit of regularized operators
 
 ## iv. References
 
@@ -501,5 +502,99 @@ lemma radiusPowUnboundedOperator_apply_ae {d : ℕ} (s : ℝ) (ψ : (ℛ[d] s).d
     ℛ s ψ =ᵐ[volume] 𝐫 s (polyBddSchwartzEquiv.symm ψ) :=
   radiusPowOperatorSchwartz_apply_ae ψ
 
+/-!
+### B.3.1. As limit of regularized operators
+-/
+
+open ENNReal in
+lemma radiusRegPowUnbounded_tendsto_radiusPowUnbounded {d : ℕ} (hd : 0 < d) {s : ℝ}
+    {ψ : schwartzSubmodule d} (hψ : ↑ψ ∈ polyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat) :
+    Tendsto (fun ε ↦ ℛ₀ ε s ψ) nhdsZeroUnits (nhds (ℛ s ⟨ψ, hψ⟩)) := by
+  have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc
+  apply tendsto_sub_nhds_zero_iff.mp
+  apply tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq.mpr
+  obtain ⟨f, hf⟩ := polyBddSchwartzEquiv.surjective ⟨ψ.1, hψ⟩
+  have hf' := (polyBddSchwartzEquiv.symm_apply_eq.mpr hf.symm).symm
+  have h_int : ∀ ε,
+      ∫⁻ x, ‖(ℛ₀ ε s ψ - ℛ s ⟨ψ, hψ⟩).1 x‖ₑ ^ 2 = ∫⁻ x, ‖𝐫₀ ε s f x - 𝐫 s f.1 x‖ₑ ^ 2 := by
+    intro ε
+    refine lintegral_congr_ae ?_
+    filter_upwards [radiusRegPowUnboundedOperator_apply_ae_eq ε s ψ,
+      radiusPowUnboundedOperator_apply_ae s ⟨ψ, hψ⟩,
+      AEEqFun.coeFn_sub (ℛ₀ ε s ψ).val (ℛ s ⟨ψ, hψ⟩).val] with x h₁ h₂ h₃
+    simp only [h₁, h₂, h₃, AddSubgroupClass.coe_sub, Pi.sub_apply, hf']
+    congr
+    exact (polyBddSchwartzEquiv_symm_apply_coe hψ).symm
+  simp_rw [h_int]
+  rw [(lintegral_zero (α := Space d) (μ := volume)).symm] -- change `0` to `∫⁻ x, 0` for dom.convg.
+  have h_meas : ∀ᶠ ε in nhdsZeroUnits, Measurable fun x ↦ ‖𝐫₀ ε s f x - 𝐫 s f.1 x‖ₑ ^ 2 :=
+    Eventually.of_forall (fun _ ↦ by fun_prop)
+  have h_lim : ∀ᵐ x, Tendsto (fun ε ↦ ‖𝐫₀ ε s f x - 𝐫 s f.1 x‖ₑ ^ 2) nhdsZeroUnits (nhds 0) := by
+    filter_upwards [radiusRegPow_ae_tendsto_radiusPow hd s f] with x h
+    apply tendsto_sub_nhds_zero_iff.mpr at h
+    have := h.enorm.ennrpow_const 2
+    simp_all
+  have hpow : ∀ x : Space d, ‖x‖ ^ s = (‖x‖ ^ 2) ^ (s / 2) := by
+    simp [← Real.rpow_natCast_mul (norm_nonneg _), mul_div_cancel₀]
+  -- Use dominated convergence theorem with different bounds for `s` positive vs. negative
+  rcases le_or_gt 0 s with (hs | hs)
+  · let bound : Space d → ℝ≥0∞ := fun x ↦ ‖𝐫₀ 1 s f x‖ₑ ^ 2
+    refine tendsto_lintegral_filter_of_dominated_convergence bound h_meas ?_ ?_ h_lim
+    · apply eventually_iff_exists_mem.mpr
+      use {ε : ℝˣ | ε.1 ^ 2 ≤ 1}
+      refine ⟨?_, fun ε hε ↦ ?_⟩
+      · use Metric.ball (0 : ℝ) 1
+        refine ⟨IsOpen.mem_nhds Metric.isOpen_ball (by norm_num), ?_⟩
+        simp only [Metric.ball, dist_zero_right, Real.norm_eq_abs, Set.preimage_setOf_eq,
+          Units.coeHom_apply, sq_le_one_iff_abs_le_one, Set.setOf_subset_setOf]
+        exact fun _ ↦ Std.le_of_lt
+      · refine Eventually.of_forall (fun x ↦ ?_)
+        simp_rw [bound, ENNReal.pow_le_pow_left_iff two_ne_zero, enorm_le_iff_norm_le]
+        calc
+          _ = |(‖x‖ ^ 2 + ε ^ 2) ^ (s / 2) - ‖x‖ ^ s| * ‖f x‖ := by
+            simp [← sub_mul, ← Complex.ofReal_sub]
+          _ ≤ |(‖x‖ ^ 2 + ε ^ 2) ^ (s / 2)| * ‖f x‖ := by
+            refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
+            refine abs_le_abs_of_nonneg ?_ ?_
+            · rw [hpow, sub_nonneg]
+              exact Real.rpow_le_rpow (by positivity) (by nlinarith) (by linarith)
+            · exact sub_le_self _ (Real.rpow_nonneg (norm_nonneg x) _)
+          _ ≤ |(‖x‖ ^ 2 + 1 ^ 2) ^ (s / 2)| * ‖f x‖ := by
+            refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
+            refine abs_le_abs_of_nonneg ?_ ?_
+            · exact Real.rpow_nonneg (norm_sq_add_unit_sq_pos _ _).le (s / 2)
+            · exact Real.rpow_le_rpow (norm_sq_add_unit_sq_pos _ _).le (by simp_all) (by linarith)
+          _ = ‖𝐫₀ 1 s f x‖ := by simp
+    · have := pow_ne_top (n := 2) ((𝐫₀ 1 s f.1).memLp 2).2.ne
+      rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ofNat_ne_top] at this
+      simp_all [bound]
+  · let bound : Space d → ℝ≥0∞ := fun x ↦ ‖𝐫 s f x‖ₑ ^ 2
+    refine tendsto_lintegral_filter_of_dominated_convergence bound h_meas ?_ ?_ h_lim
+    · refine Eventually.of_forall (fun ε ↦ ?_)
+      apply ae_iff.mpr
+      refine measure_mono_null ?_ (measure_singleton 0)
+      intro x hx
+      by_contra hx'
+      apply hx
+      simp_rw [bound, ENNReal.pow_le_pow_left_iff two_ne_zero, enorm_le_iff_norm_le]
+      calc
+        _ = |‖x‖ ^ s - (‖x‖ ^ 2 + ε ^ 2) ^ (s / 2)| * ‖f x‖ := by
+          simp [← sub_mul, ← Complex.ofReal_sub, abs_sub_comm]
+        _ ≤ |‖x‖ ^ s| * ‖f x‖ := by
+          refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
+          refine abs_le_abs_of_nonneg ?_ ?_
+          · rw [hpow, sub_nonneg]
+            refine (Real.rpow_le_rpow_iff_of_neg ?_ ?_ (by linarith)).mpr ?_
+            · exact norm_sq_add_unit_sq_pos ε x
+            · exact sq_pos_of_ne_zero (norm_ne_zero_iff.mpr hx')
+            · exact (le_add_iff_nonneg_right _).mpr (pow_two_nonneg _)
+          · rw [tsub_le_iff_right, le_add_iff_nonneg_right]
+            exact (normRegularizedPow_pos d ε s x).le
+        _ = ‖𝐫 s f x‖ := by simp
+    · have hrf := radiusPowOperator_apply_memHS s f.1 _ f.2 (add_floor_toNat_pos_aux d s)
+      have := pow_ne_top (n := 2) hrf.2.ne
+      rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ofNat_ne_top] at this
+      simp_all [bound]
+
 end
 end QuantumMechanics

From a64af97fdea8b9656c05eb3436fcda43dfe504a1 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 3 May 2026 21:26:19 +0900
Subject: [PATCH 11/12] merge fixes

---
 .../PolyBddSchwartzSubmodule.lean                 | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
index 6035e6957..fb81326ec 100644
--- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean
@@ -39,7 +39,6 @@ their being dense in `SpaceDHilbertSpace 0 ≅ ℂ`).
 - `polyBddSchwartzSubmodule d (a : ℕ∞)`: Restriction of `schwartzSubmodule d` to those Schwartz maps
   which are bounded by powers of `‖x‖`.
 - `PolyBddSchwartzSubmodule.dense d a`: These submodules are dense in `SpaceDHilbertSpace`.
-- `PolyBddSchwartzSubmodule.dense d a`: These submodules are dense in `SpaceDHilbertSpace`.
 
 ## iii. Table of contents
 
@@ -148,12 +147,11 @@ lemma polyBddSchwartzMap_zero_eq_top (d : ℕ) : polyBddSchwartzMap d 0 = ⊤ :=
 lemma polyBddSchwartzMap_antitone (d : ℕ) {a b : ℕ∞} (h : a ≤ b) :
     polyBddSchwartzMap d b ≤ polyBddSchwartzMap d a := fun _ hx k hk ↦ hx k (hk.trans h)
 
-lemma of_zero_eq (d : ℕ) :
-    polyBddSchwartzSubmodule d 0 = schwartzSubmodule d := by
+lemma of_zero_eq (d : ℕ) : polyBddSchwartzSubmodule d 0 = schwartzSubmodule d := by
   simp [polyBddSchwartzSubmodule, polyBddSchwartzIncl, polyBddSchwartzMap_zero_eq_top]
 
-lemma le_schwartzSubmodule (d : ℕ) (a : ℕ∞) :
-    polyBddSchwartzSubmodule d a ≤ schwartzSubmodule d := LinearMap.range_domRestrict_le_range _ _
+lemma le_schwartzSubmodule (d : ℕ) (a : ℕ∞) : polyBddSchwartzSubmodule d a ≤ schwartzSubmodule d :=
+  LinearMap.range_domRestrict_le_range _ _
 
 lemma antitone (d : ℕ) {a b : ℕ∞} (h : a ≤ b) :
     polyBddSchwartzSubmodule d b ≤ polyBddSchwartzSubmodule d a := by
@@ -187,8 +185,7 @@ private lemma dense_zero_top :
   · simp
   · simp [hk', add_nonneg]
 
-lemma dense_top (d : ℕ) :
-    Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDHilbertSpace d)) := by
+lemma dense_top (d : ℕ) : Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDHilbertSpace d)) := by
   rcases eq_zero_or_pos d with (rfl | hd)
   · -- `d = 0`: Every function `Space 0 ≅ {0} → ℂ` is in `polyBddSchwartzSubmodule 0 ⊤`.
     exact dense_zero_top
@@ -197,7 +194,6 @@ lemma dense_top (d : ℕ) :
     apply mem_closure_iff_seq_limit.mpr
     -- `ψₙ = [fₙ]` is a sequence in `schwartzSubmodule` which tends to `ξ`
     obtain ⟨ψ, hψ, hψξ⟩ := mem_closure_iff_seq_limit.mp (SchwartzSubmodule.dense d ξ)
-    obtain ⟨ψ, hψ, hψξ⟩ := mem_closure_iff_seq_limit.mp (SchwartzSubmodule.dense d ξ)
     let f (n : ℕ) : 𝓢(Space d, ℂ) := schwartzEquiv.symm ⟨ψ n, hψ n⟩
     -- `bₙ` is a sequence of bump functions with shrinking domain
     let b (n : ℕ) : ContDiffBump (0 : Space d) :=
@@ -290,8 +286,7 @@ lemma dense_top (d : ℕ) :
         simp_rw [h, h', Pi.sub_apply, hg, s, ← mul_sub]
         exact ENNReal.pow_le_pow_left <| enorm_bump_mul_le_enorm (b n) (fun x ↦ f n x - ξ x) x
 
-lemma dense (d : ℕ) (a : ℕ∞) :
-    Dense (polyBddSchwartzSubmodule d a : Set (SpaceDHilbertSpace d)) :=
+lemma dense (d : ℕ) (a : ℕ∞) : Dense (polyBddSchwartzSubmodule d a : Set (SpaceDHilbertSpace d)) :=
   (dense_top d).mono (antitone d le_top)
 
 end PolyBddSchwartzSubmodule

From 61b51b53b24c0ca719c54659ad36946759bb32ac Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Tue, 5 May 2026 08:50:45 +0900
Subject: [PATCH 12/12] split radius defn

---
 .../DDimensions/Operators/Position.lean             | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
index 4f38f34a0..3eba9925b 100644
--- a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
+++ b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean
@@ -452,18 +452,23 @@ lemma radiusRegPowUnboundedOperator_apply_ae_eq {d : ℕ} (ε : ℝˣ) (s : ℝ)
 
 open Complex
 
-lemma add_floor_toNat_pos_aux (d : ℕ) (s : ℝ) : 0 < d + 2 * (⌊1 - d / 2 - s⌋.toNat + s) := by
+private lemma add_floor_toNat_pos_aux (d : ℕ) (s : ℝ) :
+    0 < d + 2 * (⌊1 - d / 2 - s⌋.toNat + s) := by
   let n : ℤ := ⌊1 - d / 2 - s⌋
   have hn₁ : 1 - d / 2 - s < n + 1 := Int.lt_floor_add_one _
   have hn₂ : (n : ℝ) ≤ n.toNat := Int.cast_le.mpr (Int.self_le_toNat _)
   linarith
 
+lemma radiusPowOperator_apply_polyBddSchwartz_memHS {d : ℕ} {s : ℝ}
+    (ψ : polyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat) :
+    MemHS (𝐫[d] s (polyBddSchwartzEquiv.symm ψ)) :=
+  let f := polyBddSchwartzEquiv.symm ψ
+  radiusPowOperator_apply_memHS s f.1 ⌊1 - d / 2 - s⌋.toNat f.2 (add_floor_toNat_pos_aux d s)
+
 /-- Radius operator acting on a polynomially-bounded Schwartz submodule. -/
 def radiusPowOperatorSchwartz {d : ℕ} (s : ℝ) :
     polyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat →ₗ[ℂ] SpaceDHilbertSpace d where
-  toFun ψ :=
-    let f := polyBddSchwartzEquiv.symm ψ
-    mk <| radiusPowOperator_apply_memHS s f.1 _ f.2 (add_floor_toNat_pos_aux d s)
+  toFun ψ := mk (radiusPowOperator_apply_polyBddSchwartz_memHS ψ)
   map_add' := by simp [← mk_add]
   map_smul' := by simp [← mk_const_smul]