diff --git a/Physlib.lean b/Physlib.lean index 981f36e36..3cb1a2e46 100644 --- a/Physlib.lean +++ b/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 diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean index edc2bff68..5f5a873a7 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 @@ -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 μ} : 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 new file mode 100644 index 000000000..d38d3c661 --- /dev/null +++ b/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 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