Imports
/-
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
-/
module
public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmoduleDirichlet submodule
i. Overview
In this module we define the Dirichlet submodule of SpaceDHilbertSpaceOn Ω μ consisting of
equivalence classes of Schwartz maps which vanish on frontier Ω. The frontier (or boundary)
of a set Ω contains all points whose neighborhoods always intersect with both Ω and Ωᶜ.
These serve as a convenient dense domain for operators acting on wavefunctions satisfying
homogeneous Dirichlet boundary conditions on Ω.
ii. Key results
DirichletSubmoduleOn Ω μ: The subspace of SchwartzSubmodule d μ consisting of Schwartz maps
which vanish on the frontier of Ω.
iii. Table of contents
A. Definitions
B. Contained in SchwartzSubmoduleOn
C. Density
iv. References
@[expose] public sectionA. Definitions
The Schwartz maps which vanish on frontier Ω.
def DirichletSchwartzMap : Submodule ℂ 𝓢(Space d, ℂ) where
carrier := {f : 𝓢(Space d, ℂ) | ∀ x : frontier Ω, f x = 0}
add_mem' := d:ℕΩ:Set (Space d)μ:Measure (Space d)inst✝:μ.HasTemperateGrowth⊢ ∀ {a b : 𝓢(Space d, ℂ)},
a ∈ {f | ∀ (x : ↑(frontier Ω)), f ↑x = 0} →
b ∈ {f | ∀ (x : ↑(frontier Ω)), f ↑x = 0} → a + b ∈ {f | ∀ (x : ↑(frontier Ω)), f ↑x = 0} All goals completed! 🐙
zero_mem' := d:ℕΩ:Set (Space d)μ:Measure (Space d)inst✝:μ.HasTemperateGrowth⊢ 0 ∈ {f | ∀ (x : ↑(frontier Ω)), f ↑x = 0} All goals completed! 🐙
smul_mem' := d:ℕΩ:Set (Space d)μ:Measure (Space d)inst✝:μ.HasTemperateGrowth⊢ ∀ (c : ℂ) {x : 𝓢(Space d, ℂ)}, x ∈ {f | ∀ (x : ↑(frontier Ω)), f ↑x = 0} → c • x ∈ {f | ∀ (x : ↑(frontier Ω)), f ↑x = 0} All goals completed! 🐙
The submodule of the Hilbert space on Ω consisting of the equivalence classes
of Schwartz maps which vanish on frontier Ω.
abbrev DirichletSubmoduleOn : Submodule ℂ (SpaceDHilbertSpaceOn Ω μ) :=
(DirichletSchwartzMap Ω).map (subspaceProjection Ω μ ∘ₗ schwartzIncl μ)B. Contained in SchwartzSubmoduleOn
lemma le_schwartzSubmoduleOn : DirichletSubmoduleOn Ω μ ≤ SchwartzSubmoduleOn Ω μ := d:ℕΩ:Set (Space d)μ:Measure (Space d)inst✝:μ.HasTemperateGrowth⊢ DirichletSubmoduleOn Ω μ ≤ SchwartzSubmoduleOn Ω μ
d:ℕΩ:Set (Space d)μ:Measure (Space d)inst✝:μ.HasTemperateGrowthψ:↥(SpaceDHilbertSpaceOn Ω μ)hψ:ψ ∈ DirichletSubmoduleOn Ω μ⊢ ψ ∈ SchwartzSubmoduleOn Ω μ
d:ℕΩ:Set (Space d)μ:Measure (Space d)inst✝:μ.HasTemperateGrowthψ:↥(SpaceDHilbertSpaceOn Ω μ)hψ:ψ ∈ DirichletSubmoduleOn Ω μf:↥(DirichletSchwartzMap Ω)hf:(subspaceProjection Ω μ) ((schwartzIncl μ) ↑f) = ψ⊢ ψ ∈ SchwartzSubmoduleOn Ω μ
apply SchwartzSubmoduleOn.mem_iff.mpr ⟨⟨schwartzIncl μ f, d:ℕΩ:Set (Space d)μ:Measure (Space d)inst✝:μ.HasTemperateGrowthψ:↥(SpaceDHilbertSpaceOn Ω μ)hψ:ψ ∈ DirichletSubmoduleOn Ω μf:↥(DirichletSchwartzMap Ω)hf:(subspaceProjection Ω μ) ((schwartzIncl μ) ↑f) = ψ⊢ (schwartzIncl μ) ↑f ∈ SchwartzSubmodule d μ All goals completed! 🐙⟩, hf⟩C. Density
TODO "Prove that `DirichletSubmoduleOn Ω μ` is dense in `SpaceDHilbertSpaceOn Ω μ`
(perhaps with some assumptions on Ω and μ)."