diff --git a/PhysLean.lean b/PhysLean.lean
index 920ac6ecc..b45cee7ae 100644
--- a/PhysLean.lean
+++ b/PhysLean.lean
@@ -57,6 +57,7 @@ import PhysLean.Mathematics.Geometry.Metric.Riemannian.Defs
 import PhysLean.Mathematics.InnerProductSpace.Adjoint
 import PhysLean.Mathematics.InnerProductSpace.Basic
 import PhysLean.Mathematics.InnerProductSpace.Calculus
+import PhysLean.Mathematics.InnerProductSpace.Submodule
 import PhysLean.Mathematics.KroneckerDelta
 import PhysLean.Mathematics.LinearMaps
 import PhysLean.Mathematics.List
@@ -233,6 +234,9 @@ import PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum
 import PhysLean.QuantumMechanics.DDimensions.Operators.Commutation
 import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum
 import PhysLean.QuantumMechanics.DDimensions.Operators.Position
+import PhysLean.QuantumMechanics.DDimensions.Operators.Unbounded
+import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic
+import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
 import PhysLean.QuantumMechanics.FiniteTarget.Basic
 import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace
 import PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic
diff --git a/PhysLean/Mathematics/InnerProductSpace/Submodule.lean b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean
new file mode 100644
index 000000000..452258608
--- /dev/null
+++ b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean
@@ -0,0 +1,120 @@
+/-
+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
+-/
+import Mathlib.Analysis.InnerProductSpace.LinearPMap
+/-!
+
+# Submodules of `E × E`
+
+In this module we define `submoduleToLp` which reinterprets a submodule of `E × E`,
+where `E` is an inner product space, as a submodule of `WithLp 2 (E × E)`.
+This allows us to take advantage of the inner product structure, since otherwise
+by default `E × E` is given the sup norm.
+
+-/
+
+namespace InnerProductSpaceSubmodule
+
+open LinearPMap Submodule
+
+variable
+  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
+  (M : Submodule ℂ (E × E))
+
+/-- The submodule of `WithLp 2 (E × E)` defined by `M`. -/
+def submoduleToLp : Submodule ℂ (WithLp 2 (E × E)) where
+  carrier := {x | x.ofLp ∈ M}
+  add_mem' := by
+    intro a b ha hb
+    exact Submodule.add_mem M ha hb
+  zero_mem' := Submodule.zero_mem M
+  smul_mem' := by
+    intro c x hx
+    exact Submodule.smul_mem M c hx
+
+lemma mem_submodule_iff_mem_submoduleToLp (f : E × E) :
+    f ∈ M ↔ (WithLp.toLp 2 f) ∈ submoduleToLp M := Eq.to_iff rfl
+
+lemma submoduleToLp_closure :
+    (submoduleToLp M.topologicalClosure) = (submoduleToLp M).topologicalClosure := by
+  rw [Submodule.ext_iff]
+  intro x
+  rw [← mem_submodule_iff_mem_submoduleToLp]
+  change x.ofLp ∈ _root_.closure M ↔ x ∈ _root_.closure (submoduleToLp M)
+  repeat rw [mem_closure_iff_nhds]
+  constructor
+  · intro h t ht
+    apply mem_nhds_iff.mp at ht
+    rcases ht with ⟨t1, ht1, ht1', hx⟩
+    have : ∃ t' ∈ nhds x.ofLp, (∀ y ∈ t', WithLp.toLp 2 y ∈ t1) := by
+      refine Filter.eventually_iff_exists_mem.mp ?_
+      apply ContinuousAt.eventually_mem (by fun_prop) (IsOpen.mem_nhds ht1' hx)
+    rcases this with ⟨t2, ht2, ht2'⟩
+    rcases h t2 ht2 with ⟨w, hw⟩
+    use WithLp.toLp 2 w
+    exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)),
+      (mem_submodule_iff_mem_submoduleToLp M w).mpr hw.2⟩
+  · intro h t ht
+    apply mem_nhds_iff.mp at ht
+    rcases ht with ⟨t1, ht1, ht1', hx⟩
+    have : ∃ t' ∈ nhds x, (∀ y ∈ t', y.ofLp ∈ t1) := by
+      refine Filter.eventually_iff_exists_mem.mp ?_
+      exact ContinuousAt.eventually_mem (by fun_prop) (IsOpen.mem_nhds ht1' hx)
+    rcases this with ⟨t2, ht2, ht2'⟩
+    rcases h t2 ht2 with ⟨w, hw⟩
+    use w.ofLp
+    exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), (mem_toAddSubgroup (submoduleToLp M)).mp hw.2⟩
+
+lemma mem_submodule_closure_iff_mem_submoduleToLp_closure (f : E × E) :
+    f ∈ M.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp M).topologicalClosure := by
+  rw [← submoduleToLp_closure]
+  rfl
+
+lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal (f : E × E) :
+    f ∈ M.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp M)ᗮ := by
+  constructor <;> intro h
+  · rw [mem_orthogonal]
+    intro u hu
+    rw [mem_adjoint_iff] at h
+    have h' : inner ℂ u.snd f.1 = inner ℂ u.fst f.2 := by
+      rw [← sub_eq_zero]
+      exact h u.fst u.snd hu
+    simp [h']
+  · rw [mem_adjoint_iff]
+    intro a b hab
+    rw [mem_orthogonal] at h
+    have hab' := (mem_submodule_iff_mem_submoduleToLp M (a, b)).mp hab
+    have h' : inner ℂ a f.2 = inner ℂ b f.1 := by
+      rw [← sub_eq_zero, sub_eq_add_neg, ← inner_neg_right]
+      exact h (WithLp.toLp 2 (a, b)) hab'
+    simp [h']
+
+lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal (f : E × E) :
+    f ∈ M.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp M)ᗮᗮ := by
+  simp only [mem_adjoint_iff]
+  trans ∀ v, (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0
+  · constructor <;> intro h
+    · intro v hw
+      have h' := h (-v.snd) v.fst
+      rw [inner_neg_left, sub_neg_eq_add] at h'
+      apply h'
+      intro a b hab
+      rw [inner_neg_right, neg_sub_left, neg_eq_zero]
+      exact hw (WithLp.toLp 2 (a, b)) ((mem_submodule_iff_mem_submoduleToLp M (a, b)).mp hab)
+    · intro a b h'
+      rw [sub_eq_add_neg, ← inner_neg_left]
+      apply h (WithLp.toLp 2 (b, -a))
+      intro w hw
+      have hw' := h' w.fst w.snd hw
+      rw [sub_eq_zero] at hw'
+      simp [hw']
+  simp only [← mem_orthogonal]
+
+lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal (f : E × E) :
+    f ∈ M.topologicalClosure.adjoint ↔
+    WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp M).topologicalClosureᗮ := by
+  rw [mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal, submoduleToLp_closure]
+
+end InnerProductSpaceSubmodule
diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean
new file mode 100644
index 000000000..aaae63111
--- /dev/null
+++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean
@@ -0,0 +1,206 @@
+/-
+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
+-/
+import PhysLean.Mathematics.InnerProductSpace.Submodule
+import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule
+/-!
+
+# Unbounded operators
+
+In this file we define
+- `UnboundedOperator`: an unbounded operator with domain a submodule of a generic Hilbert space.
+  All unbounded operators are assumed to be both densely defined and closable.
+- The closure, `UnboundedOperator.closure`, and adjoint, `UnboundedOperator.adjoint`, with notation
+  `U† = U.adjoint`. That `U†` is densely defined is guaranteed by the closability of `U`.
+- The concept of a generalized eigenvector in `IsGeneralizedEigenvector`.
+
+We prove some basic relations, making use of the density and closability assumptions:
+- `U.closure† = U†` in `closure_adjoint_eq_adjoint`
+- `U†† = U.closure` in `adjoint_adjoint_eq_closure`
+
+## References
+
+- K. Schmüdgen, (2012). "Unbounded self-adjoint operators on Hilbert space" (Vol. 265). Springer.
+  https://doi.org/10.1007/978-94-007-4753-1
+
+-/
+
+namespace QuantumMechanics
+
+open LinearPMap Submodule
+
+/-- An `UnboundedOperator` is a linear map from a submodule of the Hilbert space
+  to the Hilbert space, assumed to be both densely defined and closable. -/
+@[ext]
+structure UnboundedOperator
+    (HS : Type*) [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS]
+    extends LinearPMap ℂ HS HS where
+  /-- The domain of an unbounded operator is dense in the Hilbert space. -/
+  dense_domain : Dense (domain : Set HS)
+  /-- An unbounded operator is closable. -/
+  is_closable : toLinearPMap.IsClosable
+
+namespace UnboundedOperator
+
+variable
+  {HS : Type*} [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS]
+  (U : UnboundedOperator HS)
+
+lemma ext' (U T : UnboundedOperator HS) (h : U.toLinearPMap = T.toLinearPMap) : U = T := by
+  apply UnboundedOperator.ext
+  · exact toSubMulAction_inj.mp (congrArg toSubMulAction (congrArg domain h))
+  · exact congr_arg_heq toFun h
+
+lemma ext_iff' (U T : UnboundedOperator HS) : U = T ↔ U.toLinearPMap = T.toLinearPMap := by
+  refine ⟨?_, UnboundedOperator.ext' U T⟩
+  intro h
+  rw [h]
+
+/-!
+### Construction of unbounded operators
+-/
+
+variable {E : Submodule ℂ HS} {hE : Dense (E : Set HS)}
+
+/-- An `UnboundedOperator` constructed from a symmetric linear map on a dense submodule `E`. -/
+def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator HS where
+  toLinearPMap := LinearPMap.mk E (E.subtype ∘ₗ f)
+  dense_domain := hE
+  is_closable := by
+    refine isClosable_iff_exists_closed_extension.mpr ?_
+    use (LinearPMap.mk E (E.subtype ∘ₗ f))†
+    exact ⟨adjoint_isClosed hE, IsFormalAdjoint.le_adjoint hE hf⟩
+
+@[simp]
+lemma ofSymmetric_apply {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (ψ : E) :
+    (ofSymmetric (hE := hE) f hf).toLinearPMap ψ = E.subtypeL (f ψ) := rfl
+
+/-!
+### Closure
+-/
+
+section Closure
+
+/-- The closure of an unbounded operator. -/
+noncomputable def closure : UnboundedOperator HS where
+  toLinearPMap := U.toLinearPMap.closure
+  dense_domain := Dense.mono (HasCore.le_domain (closureHasCore U.toLinearPMap)) U.dense_domain
+  is_closable := IsClosed.isClosable (IsClosable.closure_isClosed U.is_closable)
+
+@[simp]
+lemma closure_toLinearPMap : U.closure.toLinearPMap = U.toLinearPMap.closure := rfl
+
+/-- An unbounded operator is closed iff the graph of its defining LinearPMap is closed. -/
+def IsClosed : Prop := U.toLinearPMap.IsClosed
+
+lemma closure_isClosed : U.closure.IsClosed := IsClosable.closure_isClosed U.is_closable
+
+end Closure
+
+/-!
+### Adjoints
+-/
+
+section Adjoints
+
+open InnerProductSpaceSubmodule
+
+/-- The adjoint of a densely defined, closable `LinearPMap` is densely defined. -/
+lemma adjoint_isClosable_dense (f : LinearPMap ℂ HS HS) (h_dense : Dense (f.domain : Set HS))
+    (h_closable : f.IsClosable) : Dense (f†.domain : Set HS) := by
+  by_contra hd
+  have : ∃ x ∈ f†.domainᗮ, x ≠ 0 := by
+    apply not_forall.mp at hd
+    rcases hd with ⟨y, hy⟩
+    have hnetop : f†.domainᗮᗮ ≠ ⊤ := by
+      rw [orthogonal_orthogonal_eq_closure]
+      exact Ne.symm (ne_of_mem_of_not_mem' trivial hy)
+    have hnebot : f†.domainᗮ ≠ ⊥ := by
+      by_contra
+      apply hnetop
+      rwa [orthogonal_eq_top_iff]
+    exact exists_mem_ne_zero_of_ne_bot hnebot
+  rcases this with ⟨x, hx, hx'⟩
+  apply hx'
+  apply graph_fst_eq_zero_snd f.closure _ rfl
+  rw [← IsClosable.graph_closure_eq_closure_graph h_closable,
+    mem_submodule_closure_iff_mem_submoduleToLp_closure,
+    ← orthogonal_orthogonal_eq_closure,
+    ← mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal,
+    ← LinearPMap.adjoint_graph_eq_graph_adjoint h_dense,
+    mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal]
+  rintro ⟨y, Uy⟩ hy
+  simp only [neg_zero, WithLp.prod_inner_apply, inner_zero_right, add_zero]
+  exact hx y (mem_domain_of_mem_graph hy)
+
+/-- The adjoint of an unbounded operator, denoted as `U†`. -/
+noncomputable def adjoint : UnboundedOperator HS where
+  toLinearPMap := U.toLinearPMap.adjoint
+  dense_domain := adjoint_isClosable_dense U.toLinearPMap U.dense_domain U.is_closable
+  is_closable := IsClosed.isClosable (adjoint_isClosed U.dense_domain)
+
+@[inherit_doc]
+scoped postfix:1024 "†" => UnboundedOperator.adjoint
+
+noncomputable instance instStar : Star (UnboundedOperator HS) where
+  star := fun U ↦ U.adjoint
+
+@[simp]
+lemma adjoint_toLinearPMap : U†.toLinearPMap = U.toLinearPMap† := rfl
+
+lemma isSelfAdjoint_def : IsSelfAdjoint U ↔ U† = U := Iff.rfl
+
+lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by
+  rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def, ← adjoint_toLinearPMap,
+    UnboundedOperator.ext_iff']
+
+lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain
+
+lemma closure_adjoint_eq_adjoint : U.closure† = U† := by
+  -- Reduce to statement about graphs using density and closability assumptions
+  apply UnboundedOperator.ext'
+  apply LinearPMap.eq_of_eq_graph
+  rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.closure.dense_domain]
+  rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain]
+  rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable]
+  ext f
+  rw [mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal,
+    orthogonal_closure, mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal]
+
+lemma adjoint_adjoint_eq_closure : U†† = U.closure := by
+  -- Reduce to statement about graphs using density and closability assumptions
+  apply UnboundedOperator.ext'
+  apply LinearPMap.eq_of_eq_graph
+  rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U†.dense_domain]
+  rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain]
+  rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable]
+  ext f
+  rw [mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal,
+    orthogonal_orthogonal_eq_closure, mem_submodule_closure_iff_mem_submoduleToLp_closure]
+
+end Adjoints
+
+/-!
+### Generalized eigenvectors
+-/
+
+/-- A map `F : D(U) →L[ℂ] ℂ` is a generalized eigenvector of an unbounded operator `U`
+  if there is an eigenvalue `c` such that for all `ψ ∈ D(U)`, `F (U ψ) = c ⬝ F ψ`. -/
+def IsGeneralizedEigenvector (F : U.domain →L[ℂ] ℂ) (c : ℂ) : Prop :=
+  ∀ ψ : U.domain, ∃ ψ' : U.domain, ψ' = U.toFun ψ ∧ F ψ' = c • F ψ
+
+lemma isGeneralizedEigenvector_ofSymmetric_iff
+    {f : E →ₗ[ℂ] E} (hf : f.IsSymmetric) (F : E →L[ℂ] ℂ) (c : ℂ) :
+    IsGeneralizedEigenvector (ofSymmetric (hE := hE) f hf) F c ↔ ∀ ψ : E, F (f ψ) = c • F ψ := by
+  constructor <;> intro h ψ
+  · obtain ⟨ψ', hψ', hψ''⟩ := h ψ
+    apply SetLike.coe_eq_coe.mp at hψ'
+    subst hψ'
+    exact hψ''
+  · use f ψ
+    exact ⟨by simp, h ψ⟩
+
+end UnboundedOperator
+end QuantumMechanics
diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
new file mode 100644
index 000000000..5aeb42810
--- /dev/null
+++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
@@ -0,0 +1,151 @@
+/-
+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
+-/
+import Mathlib.Analysis.InnerProductSpace.Dual
+import Mathlib.MeasureTheory.Function.L2Space
+import PhysLean.SpaceAndTime.Space.Basic
+/-!
+
+# Hilbert space for quantum mechanics on Space d
+
+-/
+
+namespace QuantumMechanics
+
+noncomputable section
+
+/-- The Hilbert space for single-particle quantum mechanics on `Space d` is defined to be
+  `L²(Space d, ℂ)`, the space of almost-everywhere equal equivalence classes of square-integrable
+  functions from `Space d` to `ℂ`. -/
+abbrev SpaceDHilbertSpace (d : ℕ) := MeasureTheory.Lp (α := Space d) ℂ 2
+
+namespace SpaceDHilbertSpace
+open MeasureTheory
+open InnerProductSpace
+
+/-- The anti-linear map from the Hilbert space to its dual. -/
+def toBra {d : ℕ} : SpaceDHilbertSpace d →ₛₗ[starRingEnd ℂ] (StrongDual ℂ (SpaceDHilbertSpace d)) :=
+  toDual ℂ (SpaceDHilbertSpace d)
+
+@[simp]
+lemma toBra_apply (f g : SpaceDHilbertSpace d) : toBra f g = ⟪f, g⟫_ℂ := rfl
+
+/-- The anti-linear map `toBra` taking a ket to its corresponding bra is surjective. -/
+lemma toBra_surjective : Function.Surjective (toBra (d := d)) :=
+  (toDual ℂ (SpaceDHilbertSpace d)).surjective
+
+/-- The anti-linear map `toBra` taking a ket to its corresponding bra is injective. -/
+lemma toBra_injective : Function.Injective (toBra (d := d)) := by
+  intro f g h
+  simpa [toBra] using h
+
+/-!
+## Member of the Hilbert space as a property
+-/
+
+/-- The proposition `MemHS f` for a function `f : Space d → ℂ` is defined
+  to be true if the function `f` can be lifted to the Hilbert space. -/
+def MemHS (f : Space d → ℂ) : Prop := MemLp f 2
+
+lemma aeStronglyMeasurable_of_memHS {f : Space d → ℂ} (h : MemHS f) : AEStronglyMeasurable f :=
+  MemLp.aestronglyMeasurable h
+
+/-- A function `f` satisfies `MemHS f` if and only if it is almost everywhere
+  strongly measurable and square integrable. -/
+lemma memHS_iff {f : Space d → ℂ} : MemHS f ↔
+    AEStronglyMeasurable f ∧ Integrable (fun x ↦ ‖f x‖ ^ 2) := by
+  rw [MemHS, MemLp, and_congr_right]
+  intro h
+  rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
+    (NeZero.ne' 2).symm ENNReal.top_ne_ofNat.symm]
+  simp only [ENNReal.toReal_ofNat, ENNReal.rpow_ofNat]
+  have h' : AEStronglyMeasurable (fun x ↦ ‖f x‖ ^ 2) :=
+    AEStronglyMeasurable.pow (AEStronglyMeasurable.norm h) 2
+  simp [Integrable, h', HasFiniteIntegral]
+
+@[simp]
+lemma zero_memHS : MemHS (d := d) 0 := by
+  rw [memHS_iff]
+  simp only [Pi.zero_apply, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow,
+    integrable_zero, and_true]
+  fun_prop
+
+@[simp]
+lemma zero_fun_memHS : MemHS (fun _ : Space d ↦ (0 : ℂ)) := zero_memHS
+
+lemma memHS_add {f g : Space d → ℂ} (hf : MemHS f) (hg : MemHS g) : MemHS (f + g) :=
+  MemLp.add hf hg
+
+lemma memHS_const_smul {f : Space d → ℂ} {c : ℂ} (hf : MemHS f) : MemHS (c • f) :=
+  MemLp.const_smul hf c
+
+lemma memHS_of_ae {g : Space d → ℂ} (f : Space d → ℂ) (hf : MemHS f) (hfg : f =ᵐ[volume] g) :
+    MemHS g := MemLp.ae_eq hfg hf
+
+/-!
+## Construction of elements of the Hilbert space
+-/
+
+lemma aeEqFun_mk_mem_iff (f : Space d → ℂ) (hf : AEStronglyMeasurable f volume) :
+    AEEqFun.mk f hf ∈ SpaceDHilbertSpace d ↔ MemHS f := by
+  rw [Lp.mem_Lp_iff_memLp]
+  exact memLp_congr_ae (AEEqFun.coeFn_mk f hf)
+
+/-- Given a function `f : Space d → ℂ` such that `MemHS f` is true via `hf`,
+  `SpaceDHilbertSpace.mk f` is the element of the Hilbert space defined by `f`. -/
+def mk {f : Space d → ℂ} (hf : MemHS f) : SpaceDHilbertSpace d :=
+  ⟨AEEqFun.mk f hf.1, (aeEqFun_mk_mem_iff f hf.1).mpr hf⟩
+
+lemma coe_hilbertSpace_memHS (f : SpaceDHilbertSpace d) : MemHS (f : Space d → ℂ) := by
+  rw [← aeEqFun_mk_mem_iff f (Lp.aestronglyMeasurable f)]
+  have hf : f = AEEqFun.mk f (Lp.aestronglyMeasurable f) := (AEEqFun.mk_coeFn _).symm
+  exact hf ▸ f.2
+
+lemma mk_surjective (f : SpaceDHilbertSpace d) :
+    ∃ (g : Space d → ℂ) (hg : MemHS g), mk hg = f := by
+  use f, coe_hilbertSpace_memHS f
+  simp [mk]
+
+lemma coe_mk_ae {f : Space d → ℂ} (hf : MemHS f) : (mk hf) =ᵐ[volume] f :=
+  AEEqFun.coeFn_mk f hf.1
+
+lemma inner_mk_mk {f g : Space d → ℂ} (hf : MemHS f) (hg : MemHS g) :
+    ⟪mk hf, mk hg⟫_ℂ = ∫ x : Space d, starRingEnd ℂ (f x) * g x := by
+  apply integral_congr_ae
+  filter_upwards [coe_mk_ae hf, coe_mk_ae hg] with x hf hg
+  simp [hf, hg, mul_comm]
+
+@[simp]
+lemma eLpNorm_mk {f : Space d → ℂ} {hf : MemHS f} : eLpNorm (mk hf) 2 = eLpNorm f 2 :=
+  eLpNorm_congr_ae (coe_mk_ae hf)
+
+lemma mem_iff {f : Space d → ℂ} (hf : AEStronglyMeasurable f volume) :
+    AEEqFun.mk f hf ∈ SpaceDHilbertSpace d ↔ Integrable (fun x ↦ ‖f x‖ ^ 2) := by
+  rw [Lp.mem_Lp_iff_memLp, MemLp, eLpNorm_aeeqFun]
+  have h1 := AEEqFun.aestronglyMeasurable (AEEqFun.mk f hf)
+  have h2 : AEStronglyMeasurable (fun x ↦ norm (f x) ^ 2) :=
+    AEStronglyMeasurable.pow (continuous_norm.comp_aestronglyMeasurable hf) 2
+  simp only [h1]
+  simp only [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (NeZero.ne' 2).symm
+    (ENNReal.top_ne_ofNat).symm, ENNReal.toReal_ofNat, ENNReal.rpow_ofNat]
+  simp [h2, Integrable, HasFiniteIntegral]
+
+@[simp]
+lemma mk_add {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} :
+    mk (memHS_add hf hg) = mk hf + mk hg := rfl
+
+@[simp]
+lemma mk_const_smul {f : Space d → ℂ} {c : ℂ} {hf : MemHS f} :
+    mk (memHS_const_smul (c := c) hf) = c • mk hf := rfl
+
+lemma mk_eq_iff {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} :
+    mk hf = mk hg ↔ f =ᵐ[volume] g := by simp [mk]
+
+lemma ext_iff {f g : SpaceDHilbertSpace d} :
+    f = g ↔ (f : Space d → ℂ) =ᵐ[volume] (g : Space d → ℂ) := Lp.ext_iff
+
+end SpaceDHilbertSpace
+end
+end QuantumMechanics
diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean
new file mode 100644
index 000000000..b7e25c449
--- /dev/null
+++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean
@@ -0,0 +1,48 @@
+/-
+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
+-/
+import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
+import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic
+/-!
+
+# Schwartz submodule of the Hilbert space
+
+-/
+
+namespace QuantumMechanics
+namespace SpaceDHilbertSpace
+
+noncomputable section
+
+open MeasureTheory
+open InnerProductSpace
+open SchwartzMap
+
+/-- The continuous linear map including Schwartz functions into `SpaceDHilbertSpace d`. -/
+def schwartzIncl {d : ℕ} : 𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d := toLpCLM ℂ (E := Space d) ℂ 2
+
+lemma schwartzIncl_injective {d : ℕ} : Function.Injective (schwartzIncl (d := d)) :=
+  injective_toLp (E := Space d) 2
+
+lemma schwartzIncl_coe_ae {d : ℕ} (f : 𝓢(Space d, ℂ)) : f.1 =ᵐ[volume] (schwartzIncl f) :=
+  (coeFn_toLp f 2).symm
+
+lemma schwartzIncl_inner {d : ℕ} (f g : 𝓢(Space d, ℂ)) :
+    ⟪schwartzIncl f, schwartzIncl g⟫_ℂ = ∫ x : Space d, starRingEnd ℂ (f x) * g x := by
+  apply integral_congr_ae
+  filter_upwards [schwartzIncl_coe_ae f, schwartzIncl_coe_ae g] with _ hf hg
+  rw [← hf, ← hg, RCLike.inner_apply, mul_comm]
+  rfl
+
+/-- The submodule of `SpaceDHilbertSpace d` consisting of Schwartz functions. -/
+abbrev schwartzSubmodule (d : ℕ) := (schwartzIncl (d := d)).range
+
+lemma schwartzSubmodule_dense {d : ℕ} :
+    Dense (schwartzSubmodule d : Set (SpaceDHilbertSpace d)) :=
+  denseRange_toLpCLM ENNReal.top_ne_ofNat.symm
+
+end
+end SpaceDHilbertSpace
+end QuantumMechanics