From 77b200ed5621f88aaf18ee6d0c762864755c3817 Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 3 Jul 2026 10:57:04 +0900 Subject: [PATCH 1/7] normal operators --- .../DDimensions/Operators/Unbounded.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 0da5aa699..b228fd9a0 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -7,6 +7,7 @@ module public import Physlib.Mathematics.InnerProductSpace.Submodule public import Physlib.Mathematics.LinearPMap +public import Physlib.Meta.TODO.Basic /-! # Unbounded operators @@ -79,6 +80,12 @@ Results -/ +TODO "Prove that `IsStarNormal (T : H →ₗ.[ℂ] H)` is equivalent + to `T.domain = T†.domain` and `‖T x‖ = ‖T† x‖` for all `x ∈ T.domain`." + +TODO "Prove basic properties of `IsStarNormal (T : H →ₗ.[ℂ] H)`, + paralleling those for `IsSelfAdjoint (T : H →ₗ.[ℂ] H)`." + @[expose] public section namespace LinearPMap @@ -125,6 +132,8 @@ def IsEssentiallySelfAdjoint [CompleteSpace H] (T : H →ₗ.[ℂ] H) : Prop := lemma isEssentiallySelfAdjoint_def [CompleteSpace H] : T.IsEssentiallySelfAdjoint ↔ IsSelfAdjoint T.closure := Iff.rfl +lemma isStarNormal_def [CompleteSpace H] : IsStarNormal T ↔ T† * T = T * T† := isStarNormal_iff _ + /-! ## B. Basic properties -/ From e13f045fd457523a59e87067bccb167f131353a4 Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 3 Jul 2026 10:57:54 +0900 Subject: [PATCH 2/7] spectra --- .../DDimensions/Operators/Multiplication.lean | 10 ++++++++++ .../DDimensions/Operators/SpectralTheory/Basic.lean | 2 ++ 2 files changed, 12 insertions(+) diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean index 67daf3b36..76d2c9ff0 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean +++ b/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean @@ -339,6 +339,16 @@ lemma mulOperator_compRestricted_eq (f : Space d → ℂ) {g : Space d → ℂ} filter_upwards [mulOperator_apply_ae ⟨ψ, h ▸ Submodule.mem_top⟩] simp_all [mul_assoc] +/-! +## F. Spectrum +-/ + +TODO "Prove that the spectrum of the multiplication operators `𝓜 f` + is the 'essential range' of `f`." + +TODO "Prove that the spectrum of the multiplication operators `𝓜 f` + is the closure of `f.range` for continuous `f`." + end end SpaceDHilbertSpace end QuantumMechanics diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/SpectralTheory/Basic.lean b/Physlib/QuantumMechanics/DDimensions/Operators/SpectralTheory/Basic.lean index d10a099b4..06228f6a3 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/SpectralTheory/Basic.lean +++ b/Physlib/QuantumMechanics/DDimensions/Operators/SpectralTheory/Basic.lean @@ -85,6 +85,8 @@ Main results -/ +TODO "Move spectral theory definitions and lemmas over to Mathlib equivalents if/when available." + @[expose] public section namespace LinearPMap From aa90b9d4f1b9db06c07dc3e43093d1caa9b99efb Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 3 Jul 2026 10:58:08 +0900 Subject: [PATCH 3/7] momentum --- Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean index cd6fadb33..e45b7af7f 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean +++ b/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean @@ -38,6 +38,10 @@ Notation: -/ +TODO "Extend the domain of the momentum operator to the Sobolev space `H¹`." + +TODO "Prove that the momentum operator is self-adjoint (relies on 15310236534648318597)." + @[expose] public section namespace QuantumMechanics From c36a85917e5a819ef88c402ae9b4d49d5183aa6e Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 3 Jul 2026 10:58:35 +0900 Subject: [PATCH 4/7] hydrogen --- .../DDimensions/Hydrogen/Basic.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Physlib/QuantumMechanics/DDimensions/Hydrogen/Basic.lean b/Physlib/QuantumMechanics/DDimensions/Hydrogen/Basic.lean index 9396e875d..eb289c651 100644 --- a/Physlib/QuantumMechanics/DDimensions/Hydrogen/Basic.lean +++ b/Physlib/QuantumMechanics/DDimensions/Hydrogen/Basic.lean @@ -24,6 +24,24 @@ e.g. see https://doi.org/10.1103/PhysRevA.80.032507 and https://doi.org/10.1063/ -/ +TODO "Prove that the Hydrogen Hamiltonian is _not_ essentially self-adjoint for `d < 3`." + +TODO "Prove that the Hydrogen Hamiltonian is essentially self-adjoint for `d ≥ 3`." + +TODO "Prove that (the closure of) the Hydrogen Hamiltonian has eigenvalues (point spectrum) + {-½mk²ℏ⁻² / (n + ½(d - 1))² | n ∈ ℕ}. These correspond to the bound states." + +TODO "Prove that (the closure of) the Hydrogen Hamiltonian has continuous spectrum [0,∞). + These correspond to scattering states." + +TODO "Define the Rydberg formula and Lyman, Balmer, Paschen, etc. series." + +TODO "Determine the wavelengths / frequencies of the Lyman, Balmer, Paschen, etc. series." + +TODO "Analyze the Zeeman effect using first-order degenerate perturbation theory." + +TODO "Analyze the Stark effect using first-order degenerate perturbation theory." + @[expose] public section namespace QuantumMechanics From c4cfdd64770a1757362feb29fb0250ea1131ed2b Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 3 Jul 2026 10:58:57 +0900 Subject: [PATCH 5/7] operator examples --- Physlib.lean | 1 + .../DDimensions/Operators/Examples.lean | 28 +++++++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 Physlib/QuantumMechanics/DDimensions/Operators/Examples.lean diff --git a/Physlib.lean b/Physlib.lean index 4096ac4a2..3c1ab25d2 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -274,6 +274,7 @@ public import Physlib.QuantumMechanics.DDimensions.Hydrogen.LaplaceRungeLenzVect public import Physlib.QuantumMechanics.DDimensions.Operators.AngularMomentum public import Physlib.QuantumMechanics.DDimensions.Operators.Commutation public import Physlib.QuantumMechanics.DDimensions.Operators.Covariance +public import Physlib.QuantumMechanics.DDimensions.Operators.Examples public import Physlib.QuantumMechanics.DDimensions.Operators.Momentum public import Physlib.QuantumMechanics.DDimensions.Operators.Multiplication public import Physlib.QuantumMechanics.DDimensions.Operators.Position diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Examples.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Examples.lean new file mode 100644 index 000000000..de26ec44c --- /dev/null +++ b/Physlib/QuantumMechanics/DDimensions/Operators/Examples.lean @@ -0,0 +1,28 @@ +/- +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.Meta.TODO.Basic +/-! + +# Operator examples + +This is currently a stub, intended to host examples of operators with notable properties. + +-/ + +@[expose] public section + +TODO "Give an example of a closed, symmetric operator with _no_ self-adjoint extension. + The canonical example is the derivative operator `T = -i d/dx` on the half-space [0,∞) + with domain `D(T) = {ψ ∈ L²([0,∞), ℂ) | ψ(0) = 0}` (or a d-dimensional generalization)." + +TODO "Give an example of a densely defined, closed operator `T` such that each complex number + is an eigenvalue of `T†` but `T` has no eigenvalues: c.f. Schmüdgen Ch 2, exercise 9." + +TODO "Give an example of a symmetric operator `T` on `H` such that `(T + I • 1).range` + and `(T - I • 1).range` are dense in `H` but `T` is not essentially self-adjoint. + c.f. Schmüdgen Ch 3, exercise 12." From a3a24e52d282d40e01fdcf1cb4d576622a975061 Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 3 Jul 2026 10:59:12 +0900 Subject: [PATCH 6/7] harmonic oscillator --- Physlib.lean | 1 + .../DDimensions/HarmonicOscillator/Basic.lean | 35 +++++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean diff --git a/Physlib.lean b/Physlib.lean index 3c1ab25d2..5c983fbcb 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -269,6 +269,7 @@ public import Physlib.QFT.QED.AnomalyCancellation.Permutations public import Physlib.QFT.QED.AnomalyCancellation.Sorts public import Physlib.QFT.QED.AnomalyCancellation.VectorLike public import Physlib.QuantumMechanics.DDimensions.Basic +public import Physlib.QuantumMechanics.DDimensions.HarmonicOscillator.Basic public import Physlib.QuantumMechanics.DDimensions.Hydrogen.Basic public import Physlib.QuantumMechanics.DDimensions.Hydrogen.LaplaceRungeLenzVector public import Physlib.QuantumMechanics.DDimensions.Operators.AngularMomentum diff --git a/Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean new file mode 100644 index 000000000..ecd0129c1 --- /dev/null +++ b/Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean @@ -0,0 +1,35 @@ +/- +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.Meta.TODO.Basic +/-! + +# The quantum harmonic oscillator + +-/ + +@[expose] public section + +TODO "Define `HarmonicOscillator` as a structure extending `SpaceDQuantumSystem` + (c.f. `Hydrogen.Basic.lean` for an example). In general the potential is determined by + a positive-definite, real symmetric matrix `V = ½m(xᵗ·A·x)`. + Note that such matrices can always be diagonalized so perhaps it suffices to take `A` diagonal. + A special case with enhanced symmetry is the isotropic harmonic oscillator with `A = ω²·𝕀`." + +TODO "Define the raising/lowering/number operators for the quantum harmonic oscillator." + +TODO "Prove the commutation relations for the raising/lowering/number/Hamiltonian operators + of the quantum harmonic oscillator." + +TODO "Determine the spectrum of the quantum harmonic oscillator in terms of the eigenvalues + of the matrix `A ≻ 0` appearing in the potential." + +TODO "Determine the energy eigenstates of the quantum harmonic oscillator + in the 'Cartesian basis' in terms of Hermite polynomials." + +TODO "Determine the energy eigenstates of the quantum harmonic oscillator + in the 'spherical basis' in terms of spherical harmonics." From c121ff06b68c21936ba72df2c8c82966f3cf68c3 Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 3 Jul 2026 11:48:47 +0900 Subject: [PATCH 7/7] minor changes --- .../DDimensions/HarmonicOscillator/Basic.lean | 2 +- .../DDimensions/Operators/Multiplication.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean index ecd0129c1..e28fa0c1b 100644 --- a/Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean +++ b/Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean @@ -31,5 +31,5 @@ TODO "Determine the spectrum of the quantum harmonic oscillator in terms of the TODO "Determine the energy eigenstates of the quantum harmonic oscillator in the 'Cartesian basis' in terms of Hermite polynomials." -TODO "Determine the energy eigenstates of the quantum harmonic oscillator +TODO "Determine the energy eigenstates of the isotropic quantum harmonic oscillator in the 'spherical basis' in terms of spherical harmonics." diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean index 76d2c9ff0..a7933b373 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean +++ b/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean @@ -343,10 +343,10 @@ lemma mulOperator_compRestricted_eq (f : Space d → ℂ) {g : Space d → ℂ} ## F. Spectrum -/ -TODO "Prove that the spectrum of the multiplication operators `𝓜 f` +TODO "Prove that the spectrum of the multiplication operator `𝓜 f` is the 'essential range' of `f`." -TODO "Prove that the spectrum of the multiplication operators `𝓜 f` +TODO "Prove that the spectrum of the multiplication operator `𝓜 f` is the closure of `f.range` for continuous `f`." end