From f4e9ea0115aafa044216d60af65e1b30057befff Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 22 Jul 2026 17:09:02 +0900 Subject: [PATCH 1/8] begin hilbert space API-map --- .../HilbertSpaces/SpaceD/API-map.yaml | 64 +++++++++++++++++++ 1 file changed, 64 insertions(+) create mode 100644 Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml new file mode 100644 index 000000000..73957f4ca --- /dev/null +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml @@ -0,0 +1,64 @@ +version: v0.1 + +Title: Hilbert spaces on Space + +Overview: | + The Hilbert space on Space with measure μ is the $L^2$ space consisting of μ-a.e. equal + equivalence classes of complex functions which are square-integrable with respect to μ. + These Hilbert spaces are used extensively in the study of non-relativistic quantum mechanics. + +ParentAPIs: + - Space (Physlib/SpaceAndTime/Space) + +References: + +Requirements: + + - description: > + Defines Hilbert spaces on Space as instances of MeasureTheory.Lp + with MeasurableSpace.volume as the default measure. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean (SpaceDHilbertSpace) + + - description: > + Includes a proposition describing when a function may be interpreted as an element + of a Hilbert space on Space. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean (MemHS) + + - description: + Defines the subspace corresponding to complex Schwartz maps and provides functions + for moving back and forth between the complex Schwartz maps on Space + and their equivalence classes in the Hilbert space. + done: true + location: > + Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean + (SchwartzSubmodule, schwartzIncl, schwartzEquiv) + + - description: Defines the Fourier transform as a unitary map from the Hilbert space to itself. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Fourier.lean (fourierUnitary) + + - description: Defines the Sobolev subspaces. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean (SobolevSubmodule) + + - description: > + Defines sub-Hilbert spaces consisting of functions with support contained + in a subset of Space. + done: true + location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean + (SpaceDHilbertSpaceOn, subsetIncl, subsetProjection) + + - description: > + Defines subspaces corresponding to elements of the Hilbert space satisfying + Dirichlet boundary conditions on a subset of Space. + done: true + location: + Physlib/QuantumMechanics/HilbertSpaces/SpaceD/DirichletSubmodule.lean (DirichletSubmoduleOn) + + - description: > + Defines subspaces corresponding to elements of the Hilbert space satisfying + Neumann boundary conditions on a subset of Space. + done: false + location: N/A From 1708e796b4c8c69cd2656479c7bee0442456248b Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 22 Jul 2026 17:09:51 +0900 Subject: [PATCH 2/8] fix inline latex --- Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean index b0f807143..4af4b7e90 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean @@ -14,7 +14,7 @@ public import Physlib.SpaceAndTime.Space.Module ## i. Overview -The Hilbert spaces appropriate for doing quantum mechanics on `Space d` are the $$L^2$$-spaces +The Hilbert spaces appropriate for doing quantum mechanics on `Space d` are the $L^2$-spaces `SpaceDHilbertSpace d μ := Lp ℂ 2 μ`, where `μ` is some measure on `Space d`. Elements of `SpaceDHilbertSpace d μ` are _equivalence classes_ of functions `Space d → ℂ` which are square-integrable with respect to `μ`, i.e. `∫ x, ‖f x‖ ^ 2 ∂μ` is finite, and where `f` and `g` are @@ -34,7 +34,7 @@ equivalence classes, essentially dropping information about the functions on the ## ii. Key results -- `SpaceDHilbertSpace d μ` : The $$L^2$$-space on `Space d` with respect to the measure `μ`. +- `SpaceDHilbertSpace d μ` : The $L^2$-space on `Space d` with respect to the measure `μ`. - `toBra` : The linear equivalence between the Hilbert space and its dual. This is the map which sends each ket to its corresponding bra and _vice versa_. - `MemHS f μ` : The proposition capturing exactly when the function `f : Space d → ℂ` can be lifted From e59aacea48701ac05f7e00e6c5d9f816b4896ad6 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 22 Jul 2026 17:10:46 +0900 Subject: [PATCH 3/8] memHS in module doc --- Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean index 4af4b7e90..8d9f4c4be 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean @@ -20,6 +20,11 @@ Elements of `SpaceDHilbertSpace d μ` are _equivalence classes_ of functions `Sp square-integrable with respect to `μ`, i.e. `∫ x, ‖f x‖ ^ 2 ∂μ` is finite, and where `f` and `g` are in the same equivalence class if they are `μ`-a.e. equal. +The ability of a function to be interpreted as an element of `SpaceDHilbertSpace d μ` is captured +by the property `MemHS`. If one has `hf : MemHS f μ` for a function `f : Space d → ℂ` this means +that `f` is `μ`-a.e. strongly measurable and square-integrable; `mk hf` constructs the corresponding +equivalence class of `f` in `SpaceDHilbertSpace d μ`. + Given `SpaceDHilbertSpace d μ` and `Ω : Set (Space d)`, the Hilbert space `SpaceDHilbertSpaceOn Ω μ ≔ SpaceDHilbertSpace d (μ.restrict Ω)` may be interpreted as the sub-Hilbert space consisting of those vectors with domain contained in `Ω`. @@ -37,7 +42,7 @@ equivalence classes, essentially dropping information about the functions on the - `SpaceDHilbertSpace d μ` : The $L^2$-space on `Space d` with respect to the measure `μ`. - `toBra` : The linear equivalence between the Hilbert space and its dual. This is the map which sends each ket to its corresponding bra and _vice versa_. -- `MemHS f μ` : The proposition capturing exactly when the function `f : Space d → ℂ` can be lifted +- `MemHS f μ` : The proposition capturing exactly when a function `f : Space d → ℂ` can be lifted to an element of the Hilbert space. - `subspaceProjection` : The projection of `SpaceDHilbertSpace d μ` onto `SpaceDHilbertSpaceOn Ω μ`. - `subspaceIncl` : The linear isometry including `SpaceDHilbertSpaceOn Ω μ` From b7b5435a3f006dbf1c572102637bfc3b3d211886 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 22 Jul 2026 20:51:49 +0900 Subject: [PATCH 4/8] clean up SpaceDHilbertSpace(On) docstrings --- .../HilbertSpaces/SpaceD/Basic.lean | 22 ++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean index 8d9f4c4be..43aefe2aa 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean @@ -33,7 +33,6 @@ The reason is that for each `ψ` in `SpaceDHilbertSpaceOn Ω μ` we have contains a representative which vanishes on the complement of `Ω`. The linear isometry `restrictIncl Ω μ` describes this sub-Hilbert space relationship by mapping each `ψ` to this special representative in its equivalence class. - Similarly, we may project `SpaceDHilbertSpace d μ` onto `SpaceDHilbertSpaceOn Ω μ` by enlarging the equivalence classes, essentially dropping information about the functions on the complement of `Ω`. @@ -44,6 +43,9 @@ equivalence classes, essentially dropping information about the functions on the sends each ket to its corresponding bra and _vice versa_. - `MemHS f μ` : The proposition capturing exactly when a function `f : Space d → ℂ` can be lifted to an element of the Hilbert space. +- `SpaceDHilbertSpaceOn Ω μ` : An abbreviation for the Hilbert space + `SpaceDHilbertSpace d (μ.restrict Ω)` appropriate for describing the $L^2$-space of complex + functions on a subset of `Space d`. - `subspaceProjection` : The projection of `SpaceDHilbertSpace d μ` onto `SpaceDHilbertSpaceOn Ω μ`. - `subspaceIncl` : The linear isometry including `SpaceDHilbertSpaceOn Ω μ` as a sub-Hilbert space of `SpaceDHilbertspace d μ`. @@ -74,9 +76,8 @@ open Function InnerProductSpace MeasureTheory Measure Set ## A. SpaceDHilbertSpace -/ -/-- The Hilbert space for single-particle quantum mechanics on `Space d` with measure `μ` - is defined to be `L²(Space d, ℂ; μ)`, the space of `μ`-a.e. equal equivalence classes - of functions `f : Space d → ℂ` for which `∫ x, ‖f x‖² ∂μ` is finite. -/ +/-- The L²-space of `μ`-a.e. equal equivalence classes of functions `f : Space d → ℂ` + for which `∫ x, ‖f x‖² ∂μ` is finite. -/ abbrev SpaceDHilbertSpace (d : ℕ) (μ : Measure (Space d) := volume) := Lp ℂ 2 μ namespace SpaceDHilbertSpace @@ -152,7 +153,7 @@ lemma MemHS.indicator {Ω : Set (Space d)} (hΩ : MeasurableSet Ω) (hf : MemHS MemHS (Ω.indicator f) μ := MemLp.indicator hΩ hf -/-- If `f` is a member of the Hilbert space `SpaceDHilbertSpaceOn Ω μ` then the representative +/-- If `f` is a member of the Hilbert space with measure restricted to `Ω` then the representative `Ω.indicator f` which vanishes outside `Ω` is a member of `SpaceDHilbertSpace d μ`. -/ lemma MemHS.indicator_of_restrict {Ω : Set (Space d)} (hΩ : MeasurableSet Ω) (hf : MemHS f (μ.restrict Ω)) : @@ -187,13 +188,13 @@ lemma mk_sub : mk (hf.sub hg) = mk hf - mk hg := rfl @[simp] lemma mk_const_smul (c : ℂ) : mk (hf.const_smul c) = c • mk hf := rfl -lemma coeFn_mk : mk hf =ᵐ[μ] f := AEEqFun.coeFn_mk f hf.1 - lemma mk_eq_iff : mk hf = mk hg ↔ f =ᵐ[μ] g := by simp [mk] lemma mk_surjective : ∃ (f : Space d → ℂ) (hf : MemHS f μ), mk hf = ψ := ⟨ψ, memHS_coe ψ, by simp [mk]⟩ +lemma coeFn_mk : mk hf =ᵐ[μ] f := AEEqFun.coeFn_mk f hf.1 + lemma inner_mk_mk : ⟪mk hf, mk hg⟫_ℂ = ∫ x, starRingEnd ℂ (f x) * g x ∂μ := by apply integral_congr_ae filter_upwards [coeFn_mk hf, coeFn_mk hg] @@ -244,9 +245,10 @@ end SpaceDHilbertSpace TODO "Upgrade subspaceProjection to a ContinuousLinearMap when Lp.LpToLpOfMeasureLeSMul becomes available." -/-- The Hilbert space for single-particle quantum mechanics on a set `Ω ⊆ Space d` with measure `μ` - is defined to be `SpaceDHilbertSpace d (μ.restrict Ω)`, the space of `μ`-a.e. equal on `Ω` - equivalence classes of functions `f : Space d → ℂ` for which `∫ x on Ω, ‖f x‖² ∂μ` is finite. -/ +/-- The L²-space `SpaceDHilbertSpace d (μ.restrict Ω)`. + + Elements are equivalence classes of functions which agree `μ`-a.e. on `Ω` and which have + `∫ x in Ω, ‖f x‖ ^ 2 ∂μ` finite. -/ abbrev SpaceDHilbertSpaceOn {d : ℕ} (Ω : Set (Space d)) (μ : Measure (Space d) := volume) := SpaceDHilbertSpace d (μ.restrict Ω) From 336bb7ebeea2eafd24e9700296c7aa81029faf03 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 22 Jul 2026 20:52:06 +0900 Subject: [PATCH 5/8] homogeneous bcs --- .../HilbertSpaces/SpaceD/API-map.yaml | 20 ++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml index 73957f4ca..023a9660c 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml @@ -5,7 +5,7 @@ Title: Hilbert spaces on Space Overview: | The Hilbert space on Space with measure μ is the $L^2$ space consisting of μ-a.e. equal equivalence classes of complex functions which are square-integrable with respect to μ. - These Hilbert spaces are used extensively in the study of non-relativistic quantum mechanics. + These Hilbert spaces are used extensively in non-relativistic quantum mechanics. ParentAPIs: - Space (Physlib/SpaceAndTime/Space) @@ -21,14 +21,14 @@ Requirements: location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean (SpaceDHilbertSpace) - description: > - Includes a proposition describing when a function may be interpreted as an element - of a Hilbert space on Space. + Includes a proposition describing when a function can be interpreted + as an element of a Hilbert space on Space. done: true location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean (MemHS) - description: - Defines the subspace corresponding to complex Schwartz maps and provides functions - for moving back and forth between the complex Schwartz maps on Space + Defines the subspace corresponding to complex Schwartz maps on Space + and provides functions for moving back and forth between the Schwartz maps and their equivalence classes in the Hilbert space. done: true location: > @@ -52,13 +52,19 @@ Requirements: - description: > Defines subspaces corresponding to elements of the Hilbert space satisfying - Dirichlet boundary conditions on a subset of Space. + homogeneous Dirichlet boundary conditions on a subset of Space. done: true location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/DirichletSubmodule.lean (DirichletSubmoduleOn) - description: > Defines subspaces corresponding to elements of the Hilbert space satisfying - Neumann boundary conditions on a subset of Space. + homogeneous Neumann boundary conditions on a subset of Space. + done: false + location: N/A + + - description: > + Defines subspaces corresponding to elements of the Hilbert space satisfying + homogeneous mixed boundary conditions on a subset of Space. done: false location: N/A From bef9ac557d6ae768700c511d8802f41d2ee978b4 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 22 Jul 2026 21:09:00 +0900 Subject: [PATCH 6/8] operators --- .../HilbertSpaces/SpaceD/API-map.yaml | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml index 023a9660c..4fb5bda34 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml @@ -68,3 +68,34 @@ Requirements: homogeneous mixed boundary conditions on a subset of Space. done: false location: N/A + + - description: > + Defines the multiplication operator for a general complex function of position + with maximal domain. + done: true + location: Physlib/QuantumMechanics/Operators/Multiplication.lean (mulOperator) + + - description: + Defines position operators as instances of multiplication operators with maximal domain. + done: true + location: Physlib/QuantumMechanics/Operators/Position.lean (positionOperator) + + - description: > + Defines the derivative operator for a general complex function of the wavenumber + with maximal domain. + done: false + location: N/A + + - description: > + Defines momentum and momentum-squared operators as instances of derivative operators + with maximal domain. + done: false + location: N/A + + - description: Defines angular momentum and angular momentum-squared operators. + done: false + location: N/A + + - description: Defines the reflection operator through a general hyperplane. + done: false + location: N/A From eb06216c9b2ca6ffea8ee54c94d98befca9cb17f Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 22 Jul 2026 21:10:35 +0900 Subject: [PATCH 7/8] rephrase --- .../QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml index 4fb5bda34..dc0721c2a 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml @@ -69,9 +69,8 @@ Requirements: done: false location: N/A - - description: > - Defines the multiplication operator for a general complex function of position - with maximal domain. + - description: + Defines multiplication operators with maximal domain for any complex function of position. done: true location: Physlib/QuantumMechanics/Operators/Multiplication.lean (mulOperator) @@ -80,9 +79,8 @@ Requirements: done: true location: Physlib/QuantumMechanics/Operators/Position.lean (positionOperator) - - description: > - Defines the derivative operator for a general complex function of the wavenumber - with maximal domain. + - description: + Defines derivative operators with maximal domain for any complex function of the wavenumber. done: false location: N/A From df9b1f88df3b35549dd1fecb6fd3c81a95cd2009 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 22 Jul 2026 21:43:24 +0900 Subject: [PATCH 8/8] api linter fixes --- Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml index dc0721c2a..c356e0c08 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/API-map.yaml @@ -40,15 +40,15 @@ Requirements: location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Fourier.lean (fourierUnitary) - description: Defines the Sobolev subspaces. - done: true - location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean (SobolevSubmodule) + done: false + location: N/A - description: > Defines sub-Hilbert spaces consisting of functions with support contained in a subset of Space. done: true location: Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean - (SpaceDHilbertSpaceOn, subsetIncl, subsetProjection) + (SpaceDHilbertSpaceOn, subspaceIncl, subspaceProjection) - description: > Defines subspaces corresponding to elements of the Hilbert space satisfying