diff --git a/Physlib.lean b/Physlib.lean index 4096ac4a2..5c983fbcb 100644 --- a/Physlib.lean +++ b/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 diff --git a/Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/DDimensions/HarmonicOscillator/Basic.lean new file mode 100644 index 000000000..e28fa0c1b --- /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 isotropic quantum harmonic oscillator + in the 'spherical basis' in terms of spherical harmonics." 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 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." 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 diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean index 67daf3b36..a7933b373 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 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 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 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 -/