From 176db09e08db3047da9be707963d6582861efa3b Mon Sep 17 00:00:00 2001
From: adambornemann-glitch <adambornemann@tenkai-q.com>
Date: Fri, 17 Jul 2026 16:43:07 -0400
Subject: [PATCH 1/7] feat(QuantumMechanics): Sobolev submodules of
 SpaceDHilbertSpace
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add Mathematics/Distribution/Tempered.lean with the general API for the
embedding Lp → 𝓢': Lp.toTemperedDistribution_injective, the _add/_smul/_zero
simp lemmas, and Lp.smulLeftCLM_toTemperedDistribution_eq_iff (for a
temperate-growth symbol g, the distributional identity g · φ = u holds iff
g • φ =ᵐ u).

Add SpaceD/SobolevSubmodule.lean defining sobolevSubmodule d s (H^s as a
submodule of SpaceDHilbertSpace d), with Schwartz-map membership, density,
and antitonicity in s. Add the schwartzIncl_apply rfl-lemma to
SchwartzSubmodule.lean.

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
---
 Physlib.lean                                  |   2 +
 .../Mathematics/Distribution/Tempered.lean    | 142 ++++++++++++++++++
 .../SpaceD/SchwartzSubmodule.lean             |   4 +
 .../SpaceD/SobolevSubmodule.lean              |  84 +++++++++++
 scripts/MetaPrograms/spellingWords.txt        |   2 +
 5 files changed, 234 insertions(+)
 create mode 100644 Physlib/Mathematics/Distribution/Tempered.lean
 create mode 100644 Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean

diff --git a/Physlib.lean b/Physlib.lean
index 981f36e36..7bb940ad6 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -90,6 +90,7 @@ public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap
 public import Physlib.Mathematics.DataStructures.Matrix.LieTrace
 public import Physlib.Mathematics.Distribution.Basic
 public import Physlib.Mathematics.Distribution.PowMul
+public import Physlib.Mathematics.Distribution.Tempered
 public import Physlib.Mathematics.FDerivCurry
 public import Physlib.Mathematics.Fin
 public import Physlib.Mathematics.Fin.Involutions
@@ -297,6 +298,7 @@ public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.DirichletSubmodule
 public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.Fourier
 public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.PolyBddSchwartzSubmodule
 public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule
+public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SobolevSubmodule
 public import Physlib.QuantumMechanics.Hydrogen.Basic
 public import Physlib.QuantumMechanics.Hydrogen.LaplaceRungeLenzVector
 public import Physlib.QuantumMechanics.InfiniteSquareWell.Basic
diff --git a/Physlib/Mathematics/Distribution/Tempered.lean b/Physlib/Mathematics/Distribution/Tempered.lean
new file mode 100644
index 000000000..c2a2cda3f
--- /dev/null
+++ b/Physlib/Mathematics/Distribution/Tempered.lean
@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2026 Adam Bornemann. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Bornemann
+-/
+module
+
+public import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
+public import Mathlib.Analysis.Distribution.TemperedDistribution
+/-!
+
+# The embedding of `Lp` into tempered distributions
+
+## i. Overview
+
+Mathlib provides the linear embedding `MeasureTheory.Lp.toTemperedDistribution` of `Lp`
+classes into tempered distributions, for a measure of temperate growth. In this module we
+record the basic API for this embedding in the plain-function spelling used downstream: it
+is injective, additive and commutes with scalar multiplication, and, for a symbol `g` of
+temperate growth, the distributional identity `g · φ = u` (via `smulLeftCLM`) holds iff the
+pointwise product `g • φ` is almost everywhere equal to `u`.
+
+## ii. Key results
+
+- `MeasureTheory.Lp.toTemperedDistribution_injective` : the embedding `Lp → 𝓢'` is injective.
+- `MeasureTheory.Lp.smulLeftCLM_toTemperedDistribution_eq_iff` : the distributional identity
+  `g · φ = u` (via `smulLeftCLM`) holds iff `g • ⇑φ =ᵐ ⇑u` pointwise a.e.
+  (forward direction: `MeasureTheory.Lp.smul_coeFn_ae_eq_of_smulLeftCLM_eq`).
+
+## iii. Table of contents
+
+- A. Linearity and injectivity of the embedding
+- B. Multiplication by temperate-growth symbols
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace MeasureTheory
+namespace Lp
+
+open TemperedDistribution
+open scoped SchwartzMap ENNReal
+
+variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
+  [NormedSpace ℂ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {μ : Measure E}
+  [μ.HasTemperateGrowth] {p : ℝ≥0∞} [Fact (1 ≤ p)]
+
+/-!
+## A. Linearity and injectivity of the embedding
+-/
+
+/-- The embedding of `Lp` into tempered distributions is injective. -/
+lemma toTemperedDistribution_injective [FiniteDimensional ℝ E] [IsLocallyFiniteMeasure μ] :
+    Function.Injective (toTemperedDistribution (E := E) (F := F) (p := p) (μ := μ)) :=
+  LinearMap.ker_eq_bot.mp ker_toTemperedDistributionCLM_eq_bot
+
+/- The next three lemmas restate `map_add`/`map_smul`/`map_zero` of
+`toTemperedDistributionCLM` in the plain-function spelling `Lp.toTemperedDistribution` used
+by downstream statements; the composed-CLM form does not match it syntactically. -/
+
+/-- The embedding `Lp → 𝓢'` is additive. -/
+@[simp]
+lemma toTemperedDistribution_add (ψ φ : Lp F p μ) :
+    toTemperedDistribution (ψ + φ) = toTemperedDistribution ψ + toTemperedDistribution φ :=
+  map_add (toTemperedDistributionCLM F μ p) ψ φ
+
+/-- The embedding `Lp → 𝓢'` commutes with scalar multiplication. -/
+@[simp]
+lemma toTemperedDistribution_smul (c : ℂ) (ψ : Lp F p μ) :
+    toTemperedDistribution (c • ψ) = c • toTemperedDistribution ψ :=
+  map_smul (toTemperedDistributionCLM F μ p) c ψ
+
+/-- The embedding `Lp → 𝓢'` sends zero to zero. -/
+@[simp]
+lemma toTemperedDistribution_zero :
+    toTemperedDistribution (0 : Lp F p μ) = 0 :=
+  map_zero (toTemperedDistributionCLM F μ p)
+
+/-!
+## B. Multiplication by temperate-growth symbols
+-/
+
+variable [FiniteDimensional ℝ E] [IsLocallyFiniteMeasure μ]
+
+/-- If multiplication by a temperate-growth symbol `g` sends the tempered distribution of
+`φ ∈ Lp` to (the distribution of) `u ∈ Lp`, then the pointwise product `g • φ` is almost
+everywhere equal to `u` — in particular it lies in the same `Lp` space.
+
+The hypothesis `hg` is load-bearing for the truth of the statement, not only for the proof:
+for `g` without temperate growth, `smulLeftCLM` takes its junk value `0`, the hypothesis `h`
+then forces `u = 0`, and the conclusion fails whenever `g • ⇑φ` is not a.e. zero. -/
+lemma smul_coeFn_ae_eq_of_smulLeftCLM_eq {g : E → ℂ} (hg : g.HasTemperateGrowth)
+    {φ u : Lp ℂ p μ}
+    (h : smulLeftCLM ℂ g (toTemperedDistribution φ) = toTemperedDistribution u) :
+    g • (φ : E → ℂ) =ᵐ[μ] u := by
+  have hloc : LocallyIntegrable (g • (φ : E → ℂ)) μ :=
+    locallyIntegrableOn_univ.mp <| .continuousOn_smul isOpen_univ.isLocallyClosed
+      (((Lp.memLp φ).locallyIntegrable Fact.out).locallyIntegrableOn _)
+      hg.1.continuous.continuousOn
+  refine ae_eq_of_integral_contDiff_smul_eq hloc
+    ((Lp.memLp u).locallyIntegrable Fact.out) fun t ht_diff ht_supp => ?_
+  set T : 𝓢(E, ℂ) :=
+    (ht_supp.comp_left (g := Complex.ofRealCLM) rfl).toSchwartzMap
+      (Complex.ofRealCLM.contDiff.comp ht_diff) with hT
+  have hT_apply : ∀ x, T x = (t x : ℂ) := fun x => by simp only [hT]; rfl
+  have htest := DFunLike.congr_fun h T
+  rw [smulLeftCLM_apply_apply, toTemperedDistribution_apply, toTemperedDistribution_apply]
+    at htest
+  calc ∫ x, t x • (g • (φ : E → ℂ)) x ∂μ
+      = ∫ x, SchwartzMap.smulLeftCLM ℂ g T x • (φ : E → ℂ) x ∂μ := by
+        apply integral_congr_ae
+        filter_upwards with x
+        simp only [SchwartzMap.smulLeftCLM_apply_apply hg, hT_apply, Pi.smul_apply', smul_eq_mul,
+          Complex.real_smul]
+        ring
+    _ = ∫ x, T x • (u : E → ℂ) x ∂μ := htest
+    _ = ∫ x, t x • (u : E → ℂ) x ∂μ := by
+      apply integral_congr_ae
+      filter_upwards with x
+      simp only [hT_apply, Complex.real_smul, smul_eq_mul]
+
+/-- The distributional identity `g · φ = u` (via `smulLeftCLM`) holds iff the pointwise product
+`g • φ` is almost everywhere equal to `u`. As in the forward direction
+`smul_coeFn_ae_eq_of_smulLeftCLM_eq`, the temperate-growth hypothesis `hg` is load-bearing. -/
+lemma smulLeftCLM_toTemperedDistribution_eq_iff {g : E → ℂ} (hg : g.HasTemperateGrowth)
+    {φ u : Lp ℂ p μ} :
+    smulLeftCLM ℂ g (toTemperedDistribution φ) = toTemperedDistribution u ↔
+      g • (φ : E → ℂ) =ᵐ[μ] u := by
+  refine ⟨smul_coeFn_ae_eq_of_smulLeftCLM_eq hg, fun h => ?_⟩
+  refine DFunLike.ext _ _ fun T => ?_
+  rw [smulLeftCLM_apply_apply, toTemperedDistribution_apply, toTemperedDistribution_apply]
+  refine integral_congr_ae ?_
+  filter_upwards [h] with x hx
+  simp only [SchwartzMap.smulLeftCLM_apply_apply hg, Pi.smul_apply', smul_eq_mul] at hx ⊢
+  rw [← hx]
+  ring
+
+end Lp
+end MeasureTheory
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
index 5cf9498ab..e2e9ffa0b 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
@@ -58,6 +58,10 @@ def schwartzIncl {d : ℕ} (μ : Measure (Space d)) [μ.HasTemperateGrowth] :
     𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d μ :=
   toLpCLM ℂ ℂ 2 μ
 
+/-- Applying `schwartzIncl` to a Schwartz map `g` gives its `Lp` class `g.toLp 2 μ`. -/
+lemma schwartzIncl_apply {d : ℕ} (μ : Measure (Space d)) [μ.HasTemperateGrowth]
+    (g : 𝓢(Space d, ℂ)) : schwartzIncl μ g = g.toLp 2 μ := rfl
+
 /-- The submodule of `SpaceDHilbertSpace d` corresponding to Schwartz maps. -/
 abbrev SchwartzSubmodule (d : ℕ) (μ : Measure (Space d) := volume) [μ.HasTemperateGrowth] :
     Submodule ℂ (SpaceDHilbertSpace d μ) :=
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
new file mode 100644
index 000000000..6fbbaf1f4
--- /dev/null
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2026 Adam Bornemann. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Bornemann
+-/
+module
+
+public import Mathlib.Analysis.Distribution.Sobolev
+public import Physlib.Mathematics.Distribution.Tempered
+public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule
+/-!
+
+# Sobolev submodules of `SpaceDHilbertSpace`
+
+## i. Overview
+
+In this module we define the Sobolev submodules of `SpaceDHilbertSpace`.
+
+## ii. Key results
+
+- `sobolevSubmodule d s` : the Sobolev space `H^s` as a submodule of `SpaceDHilbertSpace d`.
+- `schwartzIncl_mem_sobolevSubmodule` / `schwartzSubmodule_le_sobolevSubmodule` /
+    `sobolevSubmodule_dense` : Schwartz maps lie in every `H^s`, which is therefore dense.
+- `sobolevSubmodule_antitone` : `H^s ≤ H^s'` for `s' ≤ s`.
+
+## iii. Table of contents
+
+- A. The Sobolev submodule `H^s`
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace QuantumMechanics
+namespace SpaceDHilbertSpace
+
+open MeasureTheory TemperedDistribution
+open scoped SchwartzMap
+
+variable {d : ℕ}
+
+/-!
+## A. The Sobolev submodule `H^s`
+-/
+
+/-- The **Sobolev space** `H^s` as a submodule of `SpaceDHilbertSpace d`: the L² classes whose
+associated tempered distribution satisfies `MemSobolev s 2`. -/
+def sobolevSubmodule (d : ℕ) (s : ℝ) : Submodule ℂ (SpaceDHilbertSpace d) where
+  carrier := {ψ | MemSobolev s 2 (Lp.toTemperedDistribution ψ)}
+  add_mem' {ψ φ} hψ hφ := by simpa [Lp.toTemperedDistribution_add] using hψ.add hφ
+  zero_mem' := by simp [Lp.toTemperedDistribution_zero]
+  smul_mem' c ψ hψ := by simpa [Lp.toTemperedDistribution_smul] using hψ.smul c
+
+/-- Membership in `H^s` is the Sobolev condition on the associated tempered distribution. -/
+lemma mem_sobolevSubmodule_iff {s : ℝ} {ψ : SpaceDHilbertSpace d} :
+    ψ ∈ sobolevSubmodule d s ↔ MemSobolev s 2 (Lp.toTemperedDistribution ψ) := Iff.rfl
+
+/-- Schwartz maps lie in every Sobolev space `H^s`. -/
+lemma schwartzIncl_mem_sobolevSubmodule (s : ℝ) (g : 𝓢(Space d, ℂ)) :
+    (schwartzIncl volume g : SpaceDHilbertSpace d) ∈ sobolevSubmodule d s := by
+  rw [mem_sobolevSubmodule_iff, schwartzIncl_apply, Lp.toTemperedDistribution_toLp_eq]
+  exact g.memSobolev
+
+/-- The Schwartz submodule is contained in every Sobolev space `H^s`. -/
+lemma schwartzSubmodule_le_sobolevSubmodule (s : ℝ) :
+    SchwartzSubmodule d ≤ sobolevSubmodule d s := by
+  rintro ψ ⟨g, rfl⟩
+  exact schwartzIncl_mem_sobolevSubmodule s g
+
+/-- Every Sobolev space `H^s` is dense in `SpaceDHilbertSpace d`, containing the dense Schwartz
+submodule. -/
+lemma sobolevSubmodule_dense (s : ℝ) :
+    Dense (sobolevSubmodule d s : Set (SpaceDHilbertSpace d)) :=
+  (SchwartzSubmodule.dense d volume).mono (schwartzSubmodule_le_sobolevSubmodule s)
+
+/-- The Sobolev spaces shrink as the regularity index grows: `H^s ≤ H^s'` for `s' ≤ s`. -/
+lemma sobolevSubmodule_antitone (d : ℕ) : Antitone (sobolevSubmodule d) :=
+  fun _ _ h _ hψ => hψ.mono h
+
+end SpaceDHilbertSpace
+
+end QuantumMechanics
diff --git a/scripts/MetaPrograms/spellingWords.txt b/scripts/MetaPrograms/spellingWords.txt
index 327cae961..3500be8da 100644
--- a/scripts/MetaPrograms/spellingWords.txt
+++ b/scripts/MetaPrograms/spellingWords.txt
@@ -248,6 +248,7 @@ been
 before
 behind
 being
+bessel
 below
 benefit
 better
@@ -2474,6 +2475,7 @@ smoothly
 smoothness
 snd
 so
+sobolev
 solar
 solely
 solid

From 2035d35048499b18d016aaffe9d6375e952734f3 Mon Sep 17 00:00:00 2001
From: adambornemann-glitch <adambornemann@tenkai-q.com>
Date: Sat, 18 Jul 2026 13:53:57 -0400
Subject: [PATCH 2/7] =?UTF-8?q?refactor(QuantumMechanics):=20Per=20review:?=
 =?UTF-8?q?=20collect=20the=20Sobolev=20lemmas=20into=20a=20SobolevSubmodu?=
 =?UTF-8?q?le=20namespace=20and=20stop=20breaking=20out=20of=20the=20Space?=
 =?UTF-8?q?DHilbertSpace=20abstraction.=20Add=20toTemperedDistribution=20/?=
 =?UTF-8?q?=20toTemperedDistributionCLM=20aliases=20(E=20=3D=20Space=20d,?=
 =?UTF-8?q?=20F=20=3D=20=E2=84=82,=20p=20=3D=202=20fixed,=20mirroring=20Me?=
 =?UTF-8?q?mHS)=20with=20the=20bridge=20lemma=20SchwartzSubmodule.toTemper?=
 =?UTF-8?q?edDistribution=5FschwartzIncl=5Feq,=20and=20remove=20schwartzIn?=
 =?UTF-8?q?cl=5Fapply.=20Define=20the=20submodule=20via=20the=20CLM=20so?=
 =?UTF-8?q?=20map=5F*=20applies,=20dropping=20the=20toTemperedDistribution?=
 =?UTF-8?q?=5Fadd/smul/zero=20restatements;=20remove=20toTemperedDistribut?=
 =?UTF-8?q?ion=5Finjective.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
---
 .../Mathematics/Distribution/Tempered.lean    | 49 ++------------
 .../SpaceD/SchwartzSubmodule.lean             |  4 --
 .../SpaceD/SobolevSubmodule.lean              | 66 +++++++++++++------
 3 files changed, 52 insertions(+), 67 deletions(-)

diff --git a/Physlib/Mathematics/Distribution/Tempered.lean b/Physlib/Mathematics/Distribution/Tempered.lean
index c2a2cda3f..c18c09a99 100644
--- a/Physlib/Mathematics/Distribution/Tempered.lean
+++ b/Physlib/Mathematics/Distribution/Tempered.lean
@@ -15,22 +15,19 @@ public import Mathlib.Analysis.Distribution.TemperedDistribution
 
 Mathlib provides the linear embedding `MeasureTheory.Lp.toTemperedDistribution` of `Lp`
 classes into tempered distributions, for a measure of temperate growth. In this module we
-record the basic API for this embedding in the plain-function spelling used downstream: it
-is injective, additive and commutes with scalar multiplication, and, for a symbol `g` of
-temperate growth, the distributional identity `g · φ = u` (via `smulLeftCLM`) holds iff the
-pointwise product `g • φ` is almost everywhere equal to `u`.
+record how this embedding interacts with multiplication by temperate-growth symbols: the
+distributional identity `g · φ = u` (via `smulLeftCLM`) holds iff the pointwise product
+`g • φ` is almost everywhere equal to `u`.
 
 ## ii. Key results
 
-- `MeasureTheory.Lp.toTemperedDistribution_injective` : the embedding `Lp → 𝓢'` is injective.
 - `MeasureTheory.Lp.smulLeftCLM_toTemperedDistribution_eq_iff` : the distributional identity
   `g · φ = u` (via `smulLeftCLM`) holds iff `g • ⇑φ =ᵐ ⇑u` pointwise a.e.
   (forward direction: `MeasureTheory.Lp.smul_coeFn_ae_eq_of_smulLeftCLM_eq`).
 
 ## iii. Table of contents
 
-- A. Linearity and injectivity of the embedding
-- B. Multiplication by temperate-growth symbols
+- A. Multiplication by temperate-growth symbols
 
 ## iv. References
 
@@ -44,43 +41,11 @@ namespace Lp
 open TemperedDistribution
 open scoped SchwartzMap ENNReal
 
-variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
-  [NormedSpace ℂ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {μ : Measure E}
-  [μ.HasTemperateGrowth] {p : ℝ≥0∞} [Fact (1 ≤ p)]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
+  [BorelSpace E] {μ : Measure E} [μ.HasTemperateGrowth] {p : ℝ≥0∞} [Fact (1 ≤ p)]
 
 /-!
-## A. Linearity and injectivity of the embedding
--/
-
-/-- The embedding of `Lp` into tempered distributions is injective. -/
-lemma toTemperedDistribution_injective [FiniteDimensional ℝ E] [IsLocallyFiniteMeasure μ] :
-    Function.Injective (toTemperedDistribution (E := E) (F := F) (p := p) (μ := μ)) :=
-  LinearMap.ker_eq_bot.mp ker_toTemperedDistributionCLM_eq_bot
-
-/- The next three lemmas restate `map_add`/`map_smul`/`map_zero` of
-`toTemperedDistributionCLM` in the plain-function spelling `Lp.toTemperedDistribution` used
-by downstream statements; the composed-CLM form does not match it syntactically. -/
-
-/-- The embedding `Lp → 𝓢'` is additive. -/
-@[simp]
-lemma toTemperedDistribution_add (ψ φ : Lp F p μ) :
-    toTemperedDistribution (ψ + φ) = toTemperedDistribution ψ + toTemperedDistribution φ :=
-  map_add (toTemperedDistributionCLM F μ p) ψ φ
-
-/-- The embedding `Lp → 𝓢'` commutes with scalar multiplication. -/
-@[simp]
-lemma toTemperedDistribution_smul (c : ℂ) (ψ : Lp F p μ) :
-    toTemperedDistribution (c • ψ) = c • toTemperedDistribution ψ :=
-  map_smul (toTemperedDistributionCLM F μ p) c ψ
-
-/-- The embedding `Lp → 𝓢'` sends zero to zero. -/
-@[simp]
-lemma toTemperedDistribution_zero :
-    toTemperedDistribution (0 : Lp F p μ) = 0 :=
-  map_zero (toTemperedDistributionCLM F μ p)
-
-/-!
-## B. Multiplication by temperate-growth symbols
+## A. Multiplication by temperate-growth symbols
 -/
 
 variable [FiniteDimensional ℝ E] [IsLocallyFiniteMeasure μ]
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
index e2e9ffa0b..5cf9498ab 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
@@ -58,10 +58,6 @@ def schwartzIncl {d : ℕ} (μ : Measure (Space d)) [μ.HasTemperateGrowth] :
     𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d μ :=
   toLpCLM ℂ ℂ 2 μ
 
-/-- Applying `schwartzIncl` to a Schwartz map `g` gives its `Lp` class `g.toLp 2 μ`. -/
-lemma schwartzIncl_apply {d : ℕ} (μ : Measure (Space d)) [μ.HasTemperateGrowth]
-    (g : 𝓢(Space d, ℂ)) : schwartzIncl μ g = g.toLp 2 μ := rfl
-
 /-- The submodule of `SpaceDHilbertSpace d` corresponding to Schwartz maps. -/
 abbrev SchwartzSubmodule (d : ℕ) (μ : Measure (Space d) := volume) [μ.HasTemperateGrowth] :
     Submodule ℂ (SpaceDHilbertSpace d μ) :=
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
index 6fbbaf1f4..7e41d21f9 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
@@ -18,14 +18,17 @@ In this module we define the Sobolev submodules of `SpaceDHilbertSpace`.
 
 ## ii. Key results
 
-- `sobolevSubmodule d s` : the Sobolev space `H^s` as a submodule of `SpaceDHilbertSpace d`.
-- `schwartzIncl_mem_sobolevSubmodule` / `schwartzSubmodule_le_sobolevSubmodule` /
-    `sobolevSubmodule_dense` : Schwartz maps lie in every `H^s`, which is therefore dense.
-- `sobolevSubmodule_antitone` : `H^s ≤ H^s'` for `s' ≤ s`.
+- `toTemperedDistribution` / `toTemperedDistributionCLM` : the tempered distribution of a
+    state, aliases of the `Lp` versions with `E = Space d`, `F = ℂ` and `p = 2` fixed.
+- `SobolevSubmodule d s` : the Sobolev space `H^s` as a submodule of `SpaceDHilbertSpace d`.
+- `SobolevSubmodule.schwartzIncl_mem` / `schwartzSubmodule_le_sobolevSubmodule` /
+    `SobolevSubmodule.dense` : Schwartz maps lie in every `H^s`, which is therefore dense.
+- `SobolevSubmodule.antitone` : `H^s ≤ H^s'` for `s' ≤ s`.
 
 ## iii. Table of contents
 
-- A. The Sobolev submodule `H^s`
+- A. The tempered distribution of a state
+- B. The Sobolev submodule `H^s`
 
 ## iv. References
 
@@ -39,44 +42,65 @@ namespace SpaceDHilbertSpace
 open MeasureTheory TemperedDistribution
 open scoped SchwartzMap
 
-variable {d : ℕ}
+variable {d : ℕ} {μ : Measure (Space d)} [μ.HasTemperateGrowth]
 
 /-!
-## A. The Sobolev submodule `H^s`
+## A. The tempered distribution of a state
+-/
+
+/-- The tempered distribution associated to a state: the alias of `Lp.toTemperedDistribution`
+with `E = Space d`, `F = ℂ` and `p = 2` fixed, as `SpaceDHilbertSpace` is of `Lp`. -/
+noncomputable abbrev toTemperedDistribution (ψ : SpaceDHilbertSpace d μ) : 𝓢'(Space d, ℂ) :=
+  Lp.toTemperedDistribution ψ
+
+/-- The embedding of states into tempered distributions as a continuous linear map: the alias
+of `Lp.toTemperedDistributionCLM` with `E = Space d`, `F = ℂ` and `p = 2` fixed. -/
+noncomputable abbrev toTemperedDistributionCLM (d : ℕ) (μ : Measure (Space d) := volume)
+    [μ.HasTemperateGrowth] : SpaceDHilbertSpace d μ →L[ℂ] 𝓢'(Space d, ℂ) :=
+  Lp.toTemperedDistributionCLM ℂ μ 2
+
+/-- The tempered distribution of the L² class of a Schwartz map is the map's own tempered
+distribution. -/
+lemma SchwartzSubmodule.toTemperedDistribution_schwartzIncl_eq (g : 𝓢(Space d, ℂ)) :
+    toTemperedDistribution (schwartzIncl μ g) = g.toTemperedDistributionCLM (Space d) ℂ μ :=
+  Lp.toTemperedDistribution_toLp_eq g
+
+/-!
+## B. The Sobolev submodule `H^s`
 -/
 
 /-- The **Sobolev space** `H^s` as a submodule of `SpaceDHilbertSpace d`: the L² classes whose
 associated tempered distribution satisfies `MemSobolev s 2`. -/
-def sobolevSubmodule (d : ℕ) (s : ℝ) : Submodule ℂ (SpaceDHilbertSpace d) where
-  carrier := {ψ | MemSobolev s 2 (Lp.toTemperedDistribution ψ)}
-  add_mem' {ψ φ} hψ hφ := by simpa [Lp.toTemperedDistribution_add] using hψ.add hφ
-  zero_mem' := by simp [Lp.toTemperedDistribution_zero]
-  smul_mem' c ψ hψ := by simpa [Lp.toTemperedDistribution_smul] using hψ.smul c
+def SobolevSubmodule (d : ℕ) (s : ℝ) : Submodule ℂ (SpaceDHilbertSpace d) where
+  carrier := {ψ | MemSobolev s 2 (toTemperedDistributionCLM d volume ψ)}
+  add_mem' {ψ φ} hψ hφ := by simpa only [Set.mem_setOf_eq, map_add] using hψ.add hφ
+  zero_mem' := by simpa only [Set.mem_setOf_eq, map_zero] using memSobolev_fun_zero (Space d) ℂ s 2
+  smul_mem' c ψ hψ := by simpa only [Set.mem_setOf_eq, map_smul] using hψ.smul c
 
 /-- Membership in `H^s` is the Sobolev condition on the associated tempered distribution. -/
 lemma mem_sobolevSubmodule_iff {s : ℝ} {ψ : SpaceDHilbertSpace d} :
-    ψ ∈ sobolevSubmodule d s ↔ MemSobolev s 2 (Lp.toTemperedDistribution ψ) := Iff.rfl
+    ψ ∈ SobolevSubmodule d s ↔ MemSobolev s 2 (toTemperedDistribution ψ) := Iff.rfl
 
 /-- Schwartz maps lie in every Sobolev space `H^s`. -/
-lemma schwartzIncl_mem_sobolevSubmodule (s : ℝ) (g : 𝓢(Space d, ℂ)) :
-    (schwartzIncl volume g : SpaceDHilbertSpace d) ∈ sobolevSubmodule d s := by
-  rw [mem_sobolevSubmodule_iff, schwartzIncl_apply, Lp.toTemperedDistribution_toLp_eq]
+lemma SobolevSubmodule.schwartzIncl_mem (s : ℝ) (g : 𝓢(Space d, ℂ)) :
+    schwartzIncl volume g ∈ SobolevSubmodule d s := by
+  rw [mem_sobolevSubmodule_iff, SchwartzSubmodule.toTemperedDistribution_schwartzIncl_eq]
   exact g.memSobolev
 
 /-- The Schwartz submodule is contained in every Sobolev space `H^s`. -/
 lemma schwartzSubmodule_le_sobolevSubmodule (s : ℝ) :
-    SchwartzSubmodule d ≤ sobolevSubmodule d s := by
+    SchwartzSubmodule d ≤ SobolevSubmodule d s := by
   rintro ψ ⟨g, rfl⟩
-  exact schwartzIncl_mem_sobolevSubmodule s g
+  exact SobolevSubmodule.schwartzIncl_mem s g
 
 /-- Every Sobolev space `H^s` is dense in `SpaceDHilbertSpace d`, containing the dense Schwartz
 submodule. -/
-lemma sobolevSubmodule_dense (s : ℝ) :
-    Dense (sobolevSubmodule d s : Set (SpaceDHilbertSpace d)) :=
+lemma SobolevSubmodule.dense (s : ℝ) :
+    Dense (SobolevSubmodule d s : Set (SpaceDHilbertSpace d)) :=
   (SchwartzSubmodule.dense d volume).mono (schwartzSubmodule_le_sobolevSubmodule s)
 
 /-- The Sobolev spaces shrink as the regularity index grows: `H^s ≤ H^s'` for `s' ≤ s`. -/
-lemma sobolevSubmodule_antitone (d : ℕ) : Antitone (sobolevSubmodule d) :=
+lemma SobolevSubmodule.antitone (d : ℕ) : Antitone (SobolevSubmodule d) :=
   fun _ _ h _ hψ => hψ.mono h
 
 end SpaceDHilbertSpace

From 58a483b59d37ae795afa8e312ee2483cc990322e Mon Sep 17 00:00:00 2001
From: adambornemann-glitch <adambornemann@tenkai-q.com>
Date: Sun, 19 Jul 2026 10:40:25 -0400
Subject: [PATCH 3/7] (QuantumMechanics): Reformat per the style guide.

---
 Physlib/Mathematics/Distribution/Tempered.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Physlib/Mathematics/Distribution/Tempered.lean b/Physlib/Mathematics/Distribution/Tempered.lean
index c18c09a99..e6bd80bc3 100644
--- a/Physlib/Mathematics/Distribution/Tempered.lean
+++ b/Physlib/Mathematics/Distribution/Tempered.lean
@@ -74,13 +74,13 @@ lemma smul_coeFn_ae_eq_of_smulLeftCLM_eq {g : E → ℂ} (hg : g.HasTemperateGro
   have htest := DFunLike.congr_fun h T
   rw [smulLeftCLM_apply_apply, toTemperedDistribution_apply, toTemperedDistribution_apply]
     at htest
-  calc ∫ x, t x • (g • (φ : E → ℂ)) x ∂μ
-      = ∫ x, SchwartzMap.smulLeftCLM ℂ g T x • (φ : E → ℂ) x ∂μ := by
-        apply integral_congr_ae
-        filter_upwards with x
-        simp only [SchwartzMap.smulLeftCLM_apply_apply hg, hT_apply, Pi.smul_apply', smul_eq_mul,
-          Complex.real_smul]
-        ring
+  calc
+    _ = ∫ x, SchwartzMap.smulLeftCLM ℂ g T x • (φ : E → ℂ) x ∂μ := by
+      apply integral_congr_ae
+      filter_upwards with x
+      simp only [SchwartzMap.smulLeftCLM_apply_apply hg, hT_apply, Pi.smul_apply', smul_eq_mul,
+        Complex.real_smul]
+      ring
     _ = ∫ x, T x • (u : E → ℂ) x ∂μ := htest
     _ = ∫ x, t x • (u : E → ℂ) x ∂μ := by
       apply integral_congr_ae

From 07fa94443e4e621a6bd88f8fb330bbc40231cc0d Mon Sep 17 00:00:00 2001
From: adambornemann-glitch <adambornemann@tenkai-q.com>
Date: Sun, 19 Jul 2026 13:15:25 -0400
Subject: [PATCH 4/7] refactor(QuantumMechanics): drop the Tempered.lean
 dependency

The Sobolev submodule now rests entirely on Mathlib's Lp and MemSobolev
API; the smulLeftCLM lemmas move to the momentum PR where they are used.

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
---
 Physlib.lean                                  |   1 -
 .../Mathematics/Distribution/Tempered.lean    | 107 ------------------
 .../SpaceD/SobolevSubmodule.lean              |   1 -
 3 files changed, 109 deletions(-)
 delete mode 100644 Physlib/Mathematics/Distribution/Tempered.lean

diff --git a/Physlib.lean b/Physlib.lean
index 7bb940ad6..3cb1a2e46 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -90,7 +90,6 @@ public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap
 public import Physlib.Mathematics.DataStructures.Matrix.LieTrace
 public import Physlib.Mathematics.Distribution.Basic
 public import Physlib.Mathematics.Distribution.PowMul
-public import Physlib.Mathematics.Distribution.Tempered
 public import Physlib.Mathematics.FDerivCurry
 public import Physlib.Mathematics.Fin
 public import Physlib.Mathematics.Fin.Involutions
diff --git a/Physlib/Mathematics/Distribution/Tempered.lean b/Physlib/Mathematics/Distribution/Tempered.lean
deleted file mode 100644
index e6bd80bc3..000000000
--- a/Physlib/Mathematics/Distribution/Tempered.lean
+++ /dev/null
@@ -1,107 +0,0 @@
-/-
-Copyright (c) 2026 Adam Bornemann. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Adam Bornemann
--/
-module
-
-public import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
-public import Mathlib.Analysis.Distribution.TemperedDistribution
-/-!
-
-# The embedding of `Lp` into tempered distributions
-
-## i. Overview
-
-Mathlib provides the linear embedding `MeasureTheory.Lp.toTemperedDistribution` of `Lp`
-classes into tempered distributions, for a measure of temperate growth. In this module we
-record how this embedding interacts with multiplication by temperate-growth symbols: the
-distributional identity `g · φ = u` (via `smulLeftCLM`) holds iff the pointwise product
-`g • φ` is almost everywhere equal to `u`.
-
-## ii. Key results
-
-- `MeasureTheory.Lp.smulLeftCLM_toTemperedDistribution_eq_iff` : the distributional identity
-  `g · φ = u` (via `smulLeftCLM`) holds iff `g • ⇑φ =ᵐ ⇑u` pointwise a.e.
-  (forward direction: `MeasureTheory.Lp.smul_coeFn_ae_eq_of_smulLeftCLM_eq`).
-
-## iii. Table of contents
-
-- A. Multiplication by temperate-growth symbols
-
-## iv. References
-
--/
-
-@[expose] public section
-
-namespace MeasureTheory
-namespace Lp
-
-open TemperedDistribution
-open scoped SchwartzMap ENNReal
-
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
-  [BorelSpace E] {μ : Measure E} [μ.HasTemperateGrowth] {p : ℝ≥0∞} [Fact (1 ≤ p)]
-
-/-!
-## A. Multiplication by temperate-growth symbols
--/
-
-variable [FiniteDimensional ℝ E] [IsLocallyFiniteMeasure μ]
-
-/-- If multiplication by a temperate-growth symbol `g` sends the tempered distribution of
-`φ ∈ Lp` to (the distribution of) `u ∈ Lp`, then the pointwise product `g • φ` is almost
-everywhere equal to `u` — in particular it lies in the same `Lp` space.
-
-The hypothesis `hg` is load-bearing for the truth of the statement, not only for the proof:
-for `g` without temperate growth, `smulLeftCLM` takes its junk value `0`, the hypothesis `h`
-then forces `u = 0`, and the conclusion fails whenever `g • ⇑φ` is not a.e. zero. -/
-lemma smul_coeFn_ae_eq_of_smulLeftCLM_eq {g : E → ℂ} (hg : g.HasTemperateGrowth)
-    {φ u : Lp ℂ p μ}
-    (h : smulLeftCLM ℂ g (toTemperedDistribution φ) = toTemperedDistribution u) :
-    g • (φ : E → ℂ) =ᵐ[μ] u := by
-  have hloc : LocallyIntegrable (g • (φ : E → ℂ)) μ :=
-    locallyIntegrableOn_univ.mp <| .continuousOn_smul isOpen_univ.isLocallyClosed
-      (((Lp.memLp φ).locallyIntegrable Fact.out).locallyIntegrableOn _)
-      hg.1.continuous.continuousOn
-  refine ae_eq_of_integral_contDiff_smul_eq hloc
-    ((Lp.memLp u).locallyIntegrable Fact.out) fun t ht_diff ht_supp => ?_
-  set T : 𝓢(E, ℂ) :=
-    (ht_supp.comp_left (g := Complex.ofRealCLM) rfl).toSchwartzMap
-      (Complex.ofRealCLM.contDiff.comp ht_diff) with hT
-  have hT_apply : ∀ x, T x = (t x : ℂ) := fun x => by simp only [hT]; rfl
-  have htest := DFunLike.congr_fun h T
-  rw [smulLeftCLM_apply_apply, toTemperedDistribution_apply, toTemperedDistribution_apply]
-    at htest
-  calc
-    _ = ∫ x, SchwartzMap.smulLeftCLM ℂ g T x • (φ : E → ℂ) x ∂μ := by
-      apply integral_congr_ae
-      filter_upwards with x
-      simp only [SchwartzMap.smulLeftCLM_apply_apply hg, hT_apply, Pi.smul_apply', smul_eq_mul,
-        Complex.real_smul]
-      ring
-    _ = ∫ x, T x • (u : E → ℂ) x ∂μ := htest
-    _ = ∫ x, t x • (u : E → ℂ) x ∂μ := by
-      apply integral_congr_ae
-      filter_upwards with x
-      simp only [hT_apply, Complex.real_smul, smul_eq_mul]
-
-/-- The distributional identity `g · φ = u` (via `smulLeftCLM`) holds iff the pointwise product
-`g • φ` is almost everywhere equal to `u`. As in the forward direction
-`smul_coeFn_ae_eq_of_smulLeftCLM_eq`, the temperate-growth hypothesis `hg` is load-bearing. -/
-lemma smulLeftCLM_toTemperedDistribution_eq_iff {g : E → ℂ} (hg : g.HasTemperateGrowth)
-    {φ u : Lp ℂ p μ} :
-    smulLeftCLM ℂ g (toTemperedDistribution φ) = toTemperedDistribution u ↔
-      g • (φ : E → ℂ) =ᵐ[μ] u := by
-  refine ⟨smul_coeFn_ae_eq_of_smulLeftCLM_eq hg, fun h => ?_⟩
-  refine DFunLike.ext _ _ fun T => ?_
-  rw [smulLeftCLM_apply_apply, toTemperedDistribution_apply, toTemperedDistribution_apply]
-  refine integral_congr_ae ?_
-  filter_upwards [h] with x hx
-  simp only [SchwartzMap.smulLeftCLM_apply_apply hg, Pi.smul_apply', smul_eq_mul] at hx ⊢
-  rw [← hx]
-  ring
-
-end Lp
-end MeasureTheory
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
index 7e41d21f9..0261f196a 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
@@ -6,7 +6,6 @@ Authors: Adam Bornemann
 module
 
 public import Mathlib.Analysis.Distribution.Sobolev
-public import Physlib.Mathematics.Distribution.Tempered
 public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule
 /-!
 

From f3a11fa2766e341ba161d7cc5309acbac84bf123 Mon Sep 17 00:00:00 2001
From: adambornemann-glitch <adambornemann@tenkai-q.com>
Date: Tue, 21 Jul 2026 17:10:54 -0400
Subject: [PATCH 5/7] refactor(QuantumMechanics): Per review: rehome the
 tempered distribution API
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The tempered-distribution aliases have wider applicability than Sobolev
spaces, so they move out of SobolevSubmodule.lean:

- `toTemperedDistribution` / `toTemperedDistributionCLM` land in a new
  section A.5 (Tempered Distribution) of HilbertSpaces/SpaceD/Basic.lean,
  between A.4 (Coersions) and Misc. (now A.6).
- `SchwartzSubmodule.toTemperedDistribution_schwartzIncl_eq` lands in
  section A of HilbertSpaces/SpaceD/SchwartzSubmodule.lean, dropping an
  unneeded `[μ.IsOpenPosMeasure]` hypothesis on the way.
- SobolevSubmodule.lean keeps only the Sobolev submodule itself; its
  remaining section renumbers to A and the module docstring is trimmed.

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
---
 .../HilbertSpaces/SpaceD/Basic.lean           | 26 ++++++++++++++--
 .../SpaceD/SchwartzSubmodule.lean             |  7 ++++-
 .../SpaceD/SobolevSubmodule.lean              | 31 ++-----------------
 3 files changed, 32 insertions(+), 32 deletions(-)

diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
index edc2bff68..240d5f724 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
@@ -1,10 +1,12 @@
 /-
 Copyright (c) 2026 Gregory J. Loges. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gregory J. Loges
+Authors: Adam Bornemann, Gregory J. Loges
 -/
 module
 
+public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
+public import Mathlib.Analysis.Distribution.Sobolev
 public import Mathlib.Analysis.InnerProductSpace.Dual
 public import Mathlib.MeasureTheory.Function.L2Space
 public import Physlib.SpaceAndTime.Space.Module
@@ -50,7 +52,8 @@ equivalence classes, essentially dropping information about the functions on the
   - A.2. Membership
   - A.3. Construction of elements
   - A.4. Coersions
-  - A.5. Misc.
+  - A.5. Tempered Distribution
+  - A.6. Misc.
 - B. SpaceDHilbertSpaceOn
 
 ## iv. References
@@ -64,6 +67,7 @@ noncomputable section
 namespace QuantumMechanics
 
 open Function InnerProductSpace MeasureTheory Measure Set
+open scoped SchwartzMap
 
 /-!
 ## A. SpaceDHilbertSpace
@@ -212,7 +216,23 @@ lemma coeFn_smul : ⇑(c • ψ) =ᵐ[μ] c • ψ := Lp.coeFn_smul _ _
 end
 
 /-!
-### A.5. Misc.
+### A.5. Tempered Distribution
+-/
+variable {d : ℕ} {μ : Measure (Space d)}
+
+/-- The tempered distribution associated to a state: the alias of `Lp.toTemperedDistribution`
+with `E = Space d`, `F = ℂ` and `p = 2` fixed, as `SpaceDHilbertSpace` is of `Lp`. -/
+noncomputable abbrev toTemperedDistribution [μ.HasTemperateGrowth]
+    (ψ : SpaceDHilbertSpace d μ) : 𝓢'(Space d, ℂ) := Lp.toTemperedDistribution ψ
+
+/-- The embedding of states into tempered distributions as a continuous linear map: the alias
+of `Lp.toTemperedDistributionCLM` with `E = Space d`, `F = ℂ` and `p = 2` fixed. -/
+noncomputable abbrev toTemperedDistributionCLM (d : ℕ) (μ : Measure (Space d) := volume)
+    [μ.HasTemperateGrowth] : SpaceDHilbertSpace d μ →L[ℂ] 𝓢'(Space d, ℂ) :=
+  Lp.toTemperedDistributionCLM ℂ μ 2
+
+/-!
+### A.6. Misc.
 -/
 
 open Filter in
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
index 5cf9498ab..f490912e3 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Gregory J. Loges. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gregory J. Loges
+Authors: Adam Bornemann, Gregory J. Loges
 -/
 module
 
@@ -135,6 +135,11 @@ variable (μ) in
 lemma schwartzIncl_ker : (schwartzIncl μ).ker = (⊥ : Submodule ℂ 𝓢(Space d, ℂ)) := by
   ext; simp [← schwartzEquiv_apply_coe]
 
+omit [μ.IsOpenPosMeasure] in
+lemma toTemperedDistribution_schwartzIncl_eq :
+    toTemperedDistribution (schwartzIncl μ g) = g.toTemperedDistributionCLM (Space d) ℂ μ :=
+  Lp.toTemperedDistribution_toLp_eq g
+
 end SchwartzSubmodule
 end SpaceDHilbertSpace
 
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
index 0261f196a..d38d3c661 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
@@ -17,8 +17,6 @@ In this module we define the Sobolev submodules of `SpaceDHilbertSpace`.
 
 ## ii. Key results
 
-- `toTemperedDistribution` / `toTemperedDistributionCLM` : the tempered distribution of a
-    state, aliases of the `Lp` versions with `E = Space d`, `F = ℂ` and `p = 2` fixed.
 - `SobolevSubmodule d s` : the Sobolev space `H^s` as a submodule of `SpaceDHilbertSpace d`.
 - `SobolevSubmodule.schwartzIncl_mem` / `schwartzSubmodule_le_sobolevSubmodule` /
     `SobolevSubmodule.dense` : Schwartz maps lie in every `H^s`, which is therefore dense.
@@ -26,8 +24,7 @@ In this module we define the Sobolev submodules of `SpaceDHilbertSpace`.
 
 ## iii. Table of contents
 
-- A. The tempered distribution of a state
-- B. The Sobolev submodule `H^s`
+- A. The Sobolev submodule `H^s`
 
 ## iv. References
 
@@ -44,31 +41,10 @@ open scoped SchwartzMap
 variable {d : ℕ} {μ : Measure (Space d)} [μ.HasTemperateGrowth]
 
 /-!
-## A. The tempered distribution of a state
+## A. The Sobolev submodule `H^s`
 -/
 
-/-- The tempered distribution associated to a state: the alias of `Lp.toTemperedDistribution`
-with `E = Space d`, `F = ℂ` and `p = 2` fixed, as `SpaceDHilbertSpace` is of `Lp`. -/
-noncomputable abbrev toTemperedDistribution (ψ : SpaceDHilbertSpace d μ) : 𝓢'(Space d, ℂ) :=
-  Lp.toTemperedDistribution ψ
-
-/-- The embedding of states into tempered distributions as a continuous linear map: the alias
-of `Lp.toTemperedDistributionCLM` with `E = Space d`, `F = ℂ` and `p = 2` fixed. -/
-noncomputable abbrev toTemperedDistributionCLM (d : ℕ) (μ : Measure (Space d) := volume)
-    [μ.HasTemperateGrowth] : SpaceDHilbertSpace d μ →L[ℂ] 𝓢'(Space d, ℂ) :=
-  Lp.toTemperedDistributionCLM ℂ μ 2
-
-/-- The tempered distribution of the L² class of a Schwartz map is the map's own tempered
-distribution. -/
-lemma SchwartzSubmodule.toTemperedDistribution_schwartzIncl_eq (g : 𝓢(Space d, ℂ)) :
-    toTemperedDistribution (schwartzIncl μ g) = g.toTemperedDistributionCLM (Space d) ℂ μ :=
-  Lp.toTemperedDistribution_toLp_eq g
-
-/-!
-## B. The Sobolev submodule `H^s`
--/
-
-/-- The **Sobolev space** `H^s` as a submodule of `SpaceDHilbertSpace d`: the L² classes whose
+/-- The Sobolev space `H^s` as a submodule of `SpaceDHilbertSpace d`: the L² classes whose
 associated tempered distribution satisfies `MemSobolev s 2`. -/
 def SobolevSubmodule (d : ℕ) (s : ℝ) : Submodule ℂ (SpaceDHilbertSpace d) where
   carrier := {ψ | MemSobolev s 2 (toTemperedDistributionCLM d volume ψ)}
@@ -103,5 +79,4 @@ lemma SobolevSubmodule.antitone (d : ℕ) : Antitone (SobolevSubmodule d) :=
   fun _ _ h _ hψ => hψ.mono h
 
 end SpaceDHilbertSpace
-
 end QuantumMechanics

From 91a11155d1903dcbd34fab6e731179e197b734ac Mon Sep 17 00:00:00 2001
From: adambornemann-glitch <adambornemann@tenkai-q.com>
Date: Wed, 22 Jul 2026 16:09:16 -0400
Subject: [PATCH 6/7] Apply reviewer changes to SpaceD/Basic.lean

---
 .../HilbertSpaces/SpaceD/Basic.lean           | 20 +++++++------------
 1 file changed, 7 insertions(+), 13 deletions(-)

diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
index 240d5f724..3713debb3 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
@@ -52,8 +52,7 @@ equivalence classes, essentially dropping information about the functions on the
   - A.2. Membership
   - A.3. Construction of elements
   - A.4. Coersions
-  - A.5. Tempered Distribution
-  - A.6. Misc.
+  - A.5. Misc.
 - B. SpaceDHilbertSpaceOn
 
 ## iv. References
@@ -216,25 +215,20 @@ lemma coeFn_smul : ⇑(c • ψ) =ᵐ[μ] c • ψ := Lp.coeFn_smul _ _
 end
 
 /-!
-### A.5. Tempered Distribution
+### A.5. Misc.
 -/
+
 variable {d : ℕ} {μ : Measure (Space d)}
 
-/-- The tempered distribution associated to a state: the alias of `Lp.toTemperedDistribution`
-with `E = Space d`, `F = ℂ` and `p = 2` fixed, as `SpaceDHilbertSpace` is of `Lp`. -/
-noncomputable abbrev toTemperedDistribution [μ.HasTemperateGrowth]
+/-- The tempered distribution associated to a state. -/
+abbrev toTemperedDistribution [μ.HasTemperateGrowth]
     (ψ : SpaceDHilbertSpace d μ) : 𝓢'(Space d, ℂ) := Lp.toTemperedDistribution ψ
 
-/-- The embedding of states into tempered distributions as a continuous linear map: the alias
-of `Lp.toTemperedDistributionCLM` with `E = Space d`, `F = ℂ` and `p = 2` fixed. -/
-noncomputable abbrev toTemperedDistributionCLM (d : ℕ) (μ : Measure (Space d) := volume)
+/-- The embedding of states into tempered distributions as a continuous linear map. -/
+abbrev toTemperedDistributionCLM (d : ℕ) (μ : Measure (Space d) := volume)
     [μ.HasTemperateGrowth] : SpaceDHilbertSpace d μ →L[ℂ] 𝓢'(Space d, ℂ) :=
   Lp.toTemperedDistributionCLM ℂ μ 2
 
-/-!
-### A.6. Misc.
--/
-
 open Filter in
 lemma tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq
     {α : Type*} {l : Filter α} {ψ : α → SpaceDHilbertSpace d μ} :

From 96bc8a28cec5cc7fb42fe828873ec0830c6a9a8d Mon Sep 17 00:00:00 2001
From: adambornemann-glitch <adambornemann@tenkai-q.com>
Date: Wed, 22 Jul 2026 16:17:26 -0400
Subject: [PATCH 7/7] remove variable from B.5. Misc

---
 Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
index 3713debb3..5f5a873a7 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
@@ -218,8 +218,6 @@ end
 ### A.5. Misc.
 -/
 
-variable {d : ℕ} {μ : Measure (Space d)}
-
 /-- The tempered distribution associated to a state. -/
 abbrev toTemperedDistribution [μ.HasTemperateGrowth]
     (ψ : SpaceDHilbertSpace d μ) : 𝓢'(Space d, ℂ) := Lp.toTemperedDistribution ψ