feat(QuantumMechanics): Add TODOs

Physlib.lean

@@ -269,11 +269,13 @@ 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
 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

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 isotropic quantum harmonic oscillator
+  in the 'spherical basis' in terms of spherical harmonics."

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

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."

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

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 operator `𝓜 f`
+  is the 'essential range' of `f`."
+
+TODO "Prove that the spectrum of the multiplication operator `𝓜 f`
+  is the closure of `f.range` for continuous `f`."
+
 end
 end SpaceDHilbertSpace
 end QuantumMechanics

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

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
 -/