feat(QuantumMechanics): Sobolev submodules of SpaceDHilbertSpace

Physlib.lean

@@ -297,6 +297,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

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
@@ -64,6 +66,7 @@ noncomputable section
 namespace QuantumMechanics
 
 open Function InnerProductSpace MeasureTheory Measure Set
+open scoped SchwartzMap
 
 /-!
 ## A. SpaceDHilbertSpace
@@ -215,6 +218,15 @@ end
 ### A.5. Misc.
 -/
 
+/-- 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. -/
+abbrev toTemperedDistributionCLM (d : ℕ) (μ : Measure (Space d) := volume)
+    [μ.HasTemperateGrowth] : SpaceDHilbertSpace d μ →L[ℂ] 𝓢'(Space d, ℂ) :=
+  Lp.toTemperedDistributionCLM ℂ μ 2
+
 open Filter in
 lemma tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq
     {α : Type*} {l : Filter α} {ψ : α → SpaceDHilbertSpace d μ} :

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
 

Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean

@@ -0,0 +1,82 @@
+/-
+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.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`.
+- `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`
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace QuantumMechanics
+namespace SpaceDHilbertSpace
+
+open MeasureTheory TemperedDistribution
+open scoped SchwartzMap
+
+variable {d : ℕ} {μ : Measure (Space d)} [μ.HasTemperateGrowth]
+
+/-!
+## 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 (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 (toTemperedDistribution ψ) := Iff.rfl
+
+/-- Schwartz maps lie in every Sobolev space `H^s`. -/
+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
+  rintro ψ ⟨g, rfl⟩
+  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)) :=
+  (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

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