Skip to content

Commit e02ba31

Browse files
glogesgloges
authored
feat(QuantumMechanics): basic properties/defs for HarmonicOscillator (#1442)
* hbar simp lemmas * QHO basic * char lengths * potential function * isotropic property * operators * TOC * ladder operator file + TODOs * basic overview
1 parent 67d9820 commit e02ba31

5 files changed

Lines changed: 306 additions & 26 deletions

File tree

‎Physlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -280,6 +280,7 @@ public import Physlib.QFT.QED.AnomalyCancellation.VectorLike
280280
public import Physlib.QuantumMechanics.FiniteTarget
281281
public import Physlib.QuantumMechanics.FreeParticle.Basic
282282
public import Physlib.QuantumMechanics.HarmonicOscillator.Basic
283+
public import Physlib.QuantumMechanics.HarmonicOscillator.LadderOperators
283284
public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Basic
284285
public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Completeness
285286
public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Eigenfunction

‎Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean‎

Lines changed: 234 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -5,31 +5,252 @@ Authors: Gregory J. Loges
55
-/
66
module
77

8-
public import Physlib.Meta.TODO.Basic
8+
public import Physlib.Meta.Informal.Basic
9+
public import Physlib.QuantumMechanics.Operators.Momentum
10+
public import Physlib.QuantumMechanics.Operators.Multiplication
11+
public import Physlib.QuantumMechanics.QuantumSystem.Basic
912
/-!
1013
1114
# The quantum harmonic oscillator
1215
13-
-/
16+
## i. Overview
1417
15-
@[expose] public section
18+
The harmonic oscillator is one of the most important examples in non-relativistic quantum mechanics.
19+
It describes a particle of mass `m` subject to a positive-definite quadratic potential
20+
in `d` dimensions.
21+
22+
- `Basic.lean` : Properties of the potential, definition of isotropic oscillators,
23+
kinetic, potential and Hamiltonian operators.
24+
- `LadderOperators.lean` : Definitions of the raising/lowering/number operators
25+
and their algebraic properties.
26+
27+
## ii. Key results
1628
17-
TODO "Define `HarmonicOscillator` as a structure extending `SpaceDQuantumSystem`
18-
(c.f. `Hydrogen.Basic.lean` for an example). In general the potential is determined by
19-
a positive-definite, real symmetric matrix `V = ½m(xᵗ·A·x)`.
20-
Note that such matrices can always be diagonalized so perhaps it suffices to take `A` diagonal.
21-
A special case with enhanced symmetry is the isotropic harmonic oscillator with `A = ω²·𝕀`."
29+
## iii. Table of contents
2230
23-
TODO "Define the raising/lowering/number operators for the quantum harmonic oscillator."
31+
- A. Basic properties
32+
- A.1. Positive mass
33+
- A.2. Positive natural frequencies
34+
- B. Characteristic lengths
35+
- C. The quadratic potential function
36+
- C.1. Positive-definite matrix
37+
- C.2. Quadratic form
38+
- C.3. Potential function
39+
- D. Isotropic oscillators
40+
- E. Hilbert space
41+
- F. Operators
42+
- E.1. Kinetic energy
43+
- E.2. Potential energy
44+
- E.3. Hamiltonian
45+
- G. As a quantum system
2446
25-
TODO "Prove the commutation relations for the raising/lowering/number/Hamiltonian operators
26-
of the quantum harmonic oscillator."
47+
## iv. References
2748
28-
TODO "Determine the spectrum of the quantum harmonic oscillator in terms of the eigenvalues
29-
of the matrix `A ≻ 0` appearing in the potential."
49+
-/
50+
51+
@[expose] public section
52+
53+
TODO "Determine the spectrum of the quantum harmonic oscillator in terms of
54+
the natural frequencies and integer quantum numbers."
3055

3156
TODO "Determine the energy eigenstates of the quantum harmonic oscillator
3257
in the 'Cartesian basis' in terms of Hermite polynomials."
3358

3459
TODO "Determine the energy eigenstates of the isotropic quantum harmonic oscillator
3560
in the 'spherical basis' in terms of spherical harmonics."
61+
62+
noncomputable section
63+
namespace QuantumMechanics
64+
65+
/-- The `d`-dimensional quantum harmonic oscillator. -/
66+
structure HarmonicOscillator (d : ℕ) where
67+
/-- The mass (positive). -/
68+
m : ℝ
69+
hm : 0 < m
70+
/-- The natural frequencies (positive). -/
71+
ω : Fin d → ℝ
72+
hω : ∀ i, 0 < ω i
73+
74+
variable {d : ℕ} (Q : HarmonicOscillator d) (i : Fin d)
75+
76+
namespace HarmonicOscillator
77+
78+
open Constants SpaceDHilbertSpace MeasureTheory
79+
80+
/-!
81+
## A. Basic properties
82+
-/
83+
84+
/-!
85+
### A.1. Positive mass
86+
-/
87+
88+
@[simp]
89+
lemma m_pos : 0 < Q.m := Q.hm
90+
91+
@[simp]
92+
lemma m_nonneg : 0 ≤ Q.m := Q.hm.le
93+
94+
@[simp]
95+
lemma m_ne_zero : Q.m ≠ 0 := Q.hm.ne'
96+
97+
/-!
98+
### A.2. Positive natural frequencies
99+
-/
100+
101+
@[simp]
102+
lemma ω_pos : 0 < Q.ω i := Q.hω i
103+
104+
@[simp]
105+
lemma ω_nonneg : 0 ≤ Q.ω i := (Q.hω i).le
106+
107+
@[simp]
108+
lemma ω_ne_zero : Q.ω i ≠ 0 := (Q.hω i).ne'
109+
110+
/-!
111+
## B. Characteristic lengths
112+
-/
113+
114+
/-- The characteristic length `ξ i ≔ √ℏ / (√Q.m * √(Q.ω i))`. -/
115+
def ξ : ℝ := √ℏ / (√Q.m * √(Q.ω i))
116+
117+
lemma ξ_eq : Q.ξ i = √ℏ / (√Q.m * √(Q.ω i)) := rfl
118+
119+
@[simp]
120+
lemma ξ_pos : 0 < Q.ξ i := by simp [ξ_eq]
121+
122+
@[simp]
123+
lemma ξ_nonneg : 0 ≤ Q.ξ i := (Q.ξ_pos i).le
124+
125+
@[simp]
126+
lemma ξ_ne_zero : Q.ξ i ≠ 0 := (Q.ξ_pos i).ne'
127+
128+
lemma ξ_sq : (Q.ξ i) ^ 2 = ℏ / (Q.m * Q.ω i) := by rw [Q.ξ_eq]; field_simp; simp [← mul_rotate]
129+
130+
lemma ξ_inv : (Q.ξ i)⁻¹ = √Q.m * √(Q.ω i) / √ℏ := by simp [ξ_eq]
131+
132+
lemma ξ_inv' : (Q.ξ i)⁻¹ = Q.m * Q.ω i * Q.ξ i / ℏ := by field_simp; simp [ξ_sq, mul_assoc]
133+
134+
/-!
135+
## C. The quadratic potential function
136+
-/
137+
138+
section
139+
140+
open Matrix
141+
142+
/-!
143+
### C.1. Positive-definite matrix
144+
-/
145+
146+
/-- The positive-definite matrix defining the quadratic potential function. -/
147+
def potentialMatrix : Matrix (Fin d) (Fin d) ℝ := diagonal ((2⁻¹ * Q.m) • Q.ω ^ 2)
148+
149+
lemma potentialMatrix_eq : Q.potentialMatrix = diagonal ((2⁻¹ * Q.m) • Q.ω ^ 2) := rfl
150+
151+
lemma potentialMatrix_isHermitian : Q.potentialMatrix.IsHermitian := by simp [potentialMatrix_eq]
152+
153+
@[simp]
154+
lemma potentialMatrix_mulVec (v : Fin d → ℝ) :
155+
Q.potentialMatrix *ᵥ v = (2⁻¹ * Q.m) • (Q.ω ^ 2 * v) := by
156+
ext
157+
simp [potentialMatrix_eq, smul_mulVec, mulVec_diagonal]
158+
159+
/-!
160+
### C.2. Quadratic form
161+
-/
162+
163+
/-- The positive-definite quadratic form associated to the potential matrix. -/
164+
def potentialQuadraticForm : QuadraticForm ℝ (Fin d → ℝ) := Q.potentialMatrix.toQuadraticForm'
165+
166+
/-!
167+
### C.3. Potential function
168+
-/
169+
170+
/-- The quadratic potential function, `½m · ∑ i, ωᵢ²·xᵢ²`. -/
171+
def potentialFunction : Space d → ℝ := Q.potentialQuadraticForm ∘ Space.val
172+
173+
lemma potentialFunction_eq : Q.potentialFunction = Q.potentialQuadraticForm ∘ Space.val := rfl
174+
175+
/-- The potential function for the harmonic oscillator is a.e. strongly measurable. -/
176+
informal_lemma potentialFunction_aestronglyMeasurable where
177+
deps := [``HarmonicOscillator]
178+
tag := "QM-HO-potAESM"
179+
180+
end
181+
182+
/-!
183+
## D. Isotropic oscillators
184+
-/
185+
186+
/-- A Harmonic oscillator is isotropic if all natural frequencies are equal. -/
187+
def IsIsotropic : Prop := ∀ i j, Q.ω i = Q.ω j
188+
189+
lemma isIsotropic_def : Q.IsIsotropic ↔ ∀ i j, Q.ω i = Q.ω j := Iff.rfl
190+
191+
lemma isIsotropic_of_one (Q : HarmonicOscillator 1) : Q.IsIsotropic := by simp [isIsotropic_def]
192+
193+
/-!
194+
## E. Hilbert space
195+
-/
196+
197+
/-- The Hilbert space for the quantum harmonic oscillator. -/
198+
@[nolint unusedArguments]
199+
abbrev HS (_ : HarmonicOscillator d) : Type _ := SpaceDHilbertSpace d
200+
201+
/-!
202+
## F. Operators
203+
-/
204+
205+
/-!
206+
### F.1. Kinetic energy
207+
-/
208+
209+
/-- The kinetic energy operator, `p²/2m`. -/
210+
def kineticOperator : Q.HS →ₗ.[ℂ] Q.HS := (2 * Q.m)⁻¹ • momentumSqOperator
211+
212+
/-!
213+
### F.2. Potential energy
214+
-/
215+
216+
section
217+
218+
open MeasureTheory Complex
219+
220+
/-- The potential operator which maps `ψ` to `Q.potentialFunction • ψ`. -/
221+
def potentialOperator : Q.HS →ₗ.[ℂ] Q.HS := 𝓜 volume (ofReal ∘ Q.potentialFunction)
222+
223+
/-- The potential operators for the harmonic oscillator is self-adjoint. -/
224+
informal_lemma potentialOperator_isSelfAdjoint where
225+
deps := [``HarmonicOscillator.potentialFunction_aestronglyMeasurable]
226+
tag := "QM-HO-potSA"
227+
228+
end
229+
230+
/-!
231+
### F.3. Hamiltonian
232+
-/
233+
234+
/-- The Hamiltonian for the harmonic oscillator. -/
235+
def hamiltonian : Q.HS →ₗ.[ℂ] Q.HS := Q.kineticOperator + Q.potentialOperator
236+
237+
lemma hamiltonain_eq : Q.hamiltonian = Q.kineticOperator + Q.potentialOperator := rfl
238+
239+
/-- The Hamiltonian for the harmonic oscillator is essentially self-adjoint. -/
240+
informal_lemma hamiltonian_essentially_self_adjoint where
241+
deps := [``HarmonicOscillator.hamiltonian]
242+
tag := "QM-HO-hamESA"
243+
244+
/-!
245+
## G. As a quantum system
246+
-/
247+
248+
/-- The `d`-dimensional harmonic oscillator as a quantum system
249+
(self-adjoint Hamiltonian acting on a Hilbert space). -/
250+
informal_definition toQuantumSystem where
251+
deps := [``HarmonicOscillator.hamiltonian_essentially_self_adjoint]
252+
tag := "QM-HO-sys"
253+
254+
end HarmonicOscillator
255+
end QuantumMechanics
256+
end

‎Physlib/QuantumMechanics/HarmonicOscillator/LadderOperators.lean‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
/-
2+
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Gregory J. Loges
5+
-/
6+
module
7+
8+
public import Physlib.QuantumMechanics.HarmonicOscillator.Basic
9+
/-!
10+
11+
# Ladder operators
12+
13+
This is currently a stub, intended to house the ladder operators of the quantum harmonic oscillator.
14+
15+
-/
16+
17+
@[expose] public section
18+
19+
/-!
20+
## A. Ladder operators
21+
-/
22+
23+
TODO "Define the raising/lowering operators for the quantum harmonic oscillator."
24+
25+
TODO "Prove that the raising/lowering operators are adjoints of one another (tag as simp?)."
26+
27+
TODO "Prove the commutation relations for the ladder operators, `[a, a†] = δ`."
28+
29+
/-!
30+
## B. Number operators
31+
-/
32+
33+
TODO "Define the number operators for the quantum harmonic oscillator
34+
in terms of the ladder operators."
35+
36+
TODO "Prove that the number operators are symmetric/self-adjoint."
37+
38+
TODO "Prove the commutation relations for the number operators, `[N i, N j] = 0`."
39+
40+
TODO "Prove the commutation relations between number and ladder operators,
41+
`[N, a] = -δ a` and `[N, a†] = δ a†`."
42+
43+
/-!
44+
## C. Hamiltonian
45+
-/
46+
47+
TODO "Define a Hamiltonian in terms of the number operators."
48+
49+
TODO "Prove the commutation relations between the Hamiltonian and ladder/number operators."
50+
51+
TODO "Relate the 'number operator' Hamiltonian to the 'K + T' Hamiltonian
52+
(=/≤/≥ depending on their domains)."
53+
54+
TODO "Prove that the two Hamiltonians define the same quantum system."

‎Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/Basic.lean‎

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ module
88
public import Physlib.QuantumMechanics.Operators.OneDimension.Parity
99
public import Physlib.QuantumMechanics.Operators.OneDimension.Momentum
1010
public import Physlib.QuantumMechanics.Operators.OneDimension.Position
11-
public import Physlib.Meta.TODO.Basic
1211
/-!
1312
1413
# 1d Harmonic Oscillator
@@ -77,20 +76,22 @@ open MeasureTheory
7776
variable (Q : HarmonicOscillator)
7877

7978
@[simp]
80-
lemma m_mul_ω_div_two_ℏ_pos : 0 < Q.m * Q.ω / (2 * ℏ) := by
81-
apply div_pos
82-
· exact mul_pos Q.hm Q.hω
83-
· exact mul_pos (by norm_num) ℏ_pos
79+
lemma m_pos : 0 < Q.m := Q.hm
8480

8581
@[simp]
86-
lemma m_mul_ω_div_ℏ_pos : 0 < Q.m * Q.ω / ℏ := by
87-
apply div_pos
88-
· exact mul_pos Q.hm Q.hω
89-
· exact ℏ_pos
82+
lemma m_nonneg : 0 ≤ Q.m := Q.hm.le
83+
84+
@[simp]
85+
lemma m_ne_zero : Q.m ≠ 0 := Q.hm.ne'
86+
87+
@[simp]
88+
lemma ω_pos : 0 < Q.ω := Q.hω
9089

91-
lemma m_ne_zero : Q.m ≠ 0 := by
92-
have h1 := Q.hm
93-
linarith
90+
@[simp]
91+
lemma ω_nonneg : 0 ≤ Q.ω := Q.hω.le
92+
93+
@[simp]
94+
lemma ω_ne_zero : Q.ω ≠ 0 := Q.hω.ne'
9495

9596
/-!
9697
@@ -137,7 +138,7 @@ lemma ξ_inverse : Q.ξ⁻¹ = √(Q.m * Q.ω / ℏ) := by
137138

138139
lemma one_over_ξ_sq : (1/Q.ξ)^2 = Q.m * Q.ω / ℏ := by
139140
rw [one_over_ξ]
140-
refine Real.sq_sqrt (le_of_lt Q.m_mul_ω_div_ℏ_pos)
141+
exact Real.sq_sqrt (by simp [div_nonneg])
141142

142143
@[inherit_doc momentumOperator]
143144
scoped[QuantumMechanics.OneDimension.HarmonicOscillator] notation "Pᵒᵖ" => momentumOperator

‎Physlib/QuantumMechanics/PlanckConstant.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,12 +24,15 @@ namespace Constants
2424
def ℏ : Subtype fun x : ℝ => 0 < x := ⟨1.054571817e-34, by norm_num⟩
2525

2626
/-- Planck's constant is positive. -/
27+
@[simp]
2728
lemma ℏ_pos : 0 < (ℏ : ℝ) := ℏ.2
2829

2930
/-- Planck's constant is non-negative. -/
31+
@[simp]
3032
lemma ℏ_nonneg : 0 ≤ (ℏ : ℝ) := le_of_lt ℏ.2
3133

3234
/-- Planck's constant is not equal to zero. -/
35+
@[simp]
3336
lemma ℏ_ne_zero : (ℏ : ℝ) ≠ 0 := ne_of_gt ℏ.2
3437

3538
end Constants

0 commit comments

Comments
 (0)