1.1. Quantum Harmonic Oscillator
1.1.1. Introduction
The quantum harmonic oscillator is a fundamental example of a one-dimensional quantum mechanical system. It is often one of the first models encountered by undergraduate students studying quantum mechanics.
This note presents the formalization of the quantum harmonic oscillator in the theorem prover Lean 4, as part of the larger project PhysLean. What this means is that every definition and theorem in this note has been formally checked for mathematical correctness for by a computer. There are a number of motivations for doing this which are dicussed physlean.com
Note that we do not give every definition and theorem which is part of the formalization. Our goal is give key aspects, in such a way that we hope this note will be useful to newcomers to Lean or those intrested in simply intrested in learning about the quantum harmonic oscillator.
1.1.2. Hilbert space
The Hilbert space for a one dimensional quantum system is defined as
the space of almost-everywhere equal equivalence classes of square integrable functions
from ℝ to ℂ.
Show Lean signature:
QuantumMechanics.OneDimension.HilbertSpace
: AddSubgroup (ℝ →ₘ[MeasureTheory.volume] ℂ)
The proposition MemHS f for a function f : ℝ → ℂ is defined
to be true if the function f can be lifted to the Hilbert space.
Show Lean signature:
QuantumMechanics.OneDimension.HilbertSpace.MemHS
(f : ℝ → ℂ) : Prop
A function f satisfies MemHS f if and only if it is almost everywhere
strongly measurable, and square integrable.
Show Lean signature:
QuantumMechanics.OneDimension.HilbertSpace.memHS_iff
{f : ℝ → ℂ}
: MemHS f ↔
MeasureTheory.AEStronglyMeasurable f
MeasureTheory.volume ∧
MeasureTheory.Integrable
(fun x => ‖f x‖ ^ 2)
MeasureTheory.volume
Given a function f : ℝ → ℂ such that MemHS f is true via hf, then HilbertSpace.mk hf
is the element of the HilbertSpace defined by f.
Show Lean signature:
QuantumMechanics.OneDimension.HilbertSpace.mk
{f : ℝ → ℂ} (hf : MemHS f)
: ↥QuantumMechanics.OneDimension.HilbertSpace
The parity operator is defined as linear map from ℝ → ℂ to itself, such that
ψ is taken to fun x => ψ (-x).
Show Lean signature:
QuantumMechanics.OneDimension.HilbertSpace.parity
: (ℝ → ℂ) →ₗ[ℂ] ℝ → ℂ1.1.3. The Schrodinger Operator
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator
: TypeShow Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.ξ
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
: ℝ
For a harmonic oscillator, the Schrodinger Operator corresponding to it
is defined as the function from ℝ → ℂ to ℝ → ℂ taking
ψ ↦ - ℏ^2 / (2 * m) * ψ'' + 1/2 * m * ω^2 * x^2 * ψ.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(ψ : ℝ → ℂ) : ℝ → ℂThe Schrodinger operator commutes with the parity operator.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_parity
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(ψ : ℝ → ℂ)
: Q.schrodingerOperator (parity ψ) =
parity (Q.schrodingerOperator ψ)1.1.4. The eigenfunctions of the Schrodinger Operator
The Physicists Hermite polynomial are defined as polynomials over ℤ in X recursively
with physHermite 0 = 1 and
physHermite (n + 1) = 2 • X * physHermite n - derivative (physHermite n).
This polynomial will often be cast as a function ℝ → ℝ by evaluating the polynomial at X.
Show Lean signature:
PhysLean.physHermite : ℕ → Polynomial ℤ
The nth eigenfunction of the Harmonic oscillator is defined as the function ℝ → ℂ
taking x : ℝ to
1/√(2^n n!) 1/√(√π ξ) * physHermite n (x / ξ) * e ^ (- x²/ (2 ξ²)).
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(n : ℕ) : ℝ → ℂ1.1.5. Properties of the eigenfunctions
The eigenfunctions are integrable.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_integrable
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(n : ℕ)
: MeasureTheory.Integrable
(Q.eigenfunction n) MeasureTheory.volumeThe eigenfunctions are real.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_conj
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(n : ℕ) (x : ℝ)
: (starRingEnd ℂ) (Q.eigenfunction n x) =
Q.eigenfunction n xThe eigenfunctions are almost everywhere strongly measurable.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_aeStronglyMeasurable
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(n : ℕ)
: MeasureTheory.AEStronglyMeasurable
(Q.eigenfunction n) MeasureTheory.volumeThe eigenfunctions are square integrable.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_square_integrable
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(n : ℕ)
: MeasureTheory.Integrable
(fun x => ‖Q.eigenfunction n x‖ ^ 2)
MeasureTheory.volumeThe eigenfunctions are members of the Hilbert space.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_memHS
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(n : ℕ) : MemHS (Q.eigenfunction n)The eigenfunctions are differentiable.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_differentiableAt
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(x : ℝ) (n : ℕ)
: DifferentiableAt ℝ (Q.eigenfunction n) xThe eigenfunctions are orthonormal within the Hilbert space.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_orthonormal
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
: Orthonormal ℂ fun n =>
QuantumMechanics.OneDimension.HilbertSpace.mk
⋯
The nth eigenfunction is an eigenfunction of the parity operator with
the eigenvalue (-1) ^ n.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_parity
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(n : ℕ)
: parity (Q.eigenfunction n) =
(-1) ^ n * Q.eigenfunction n1.1.6. The time-independent Schrodinger Equation
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenValue
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(n : ℕ) : ℝ
The nth eigenfunction satisfies the time-independent Schrodinger equation with
respect to the nth eigenvalue. That is to say for Q a harmonic oscillator,
Q.schrodingerOperator (Q.eigenfunction n) x = Q.eigenValue n * Q.eigenfunction n x.
The proof of this result is done by explicit calculation of derivatives.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eigenfunction
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(n : ℕ) (x : ℝ)
: Q.schrodingerOperator (Q.eigenfunction n)
x =
↑(Q.eigenValue n) * Q.eigenfunction n x1.1.7. Completeness
If f is a function ℝ → ℂ satisfying MemHS f such that it is orthogonal
to all eigenfunction n then it is orthogonal to
x ^ r * e ^ (- x ^ 2 / (2 ξ^2))
the proof of this result relies on the fact that Hermite polynomials span polynomials.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_power_of_mem_orthogonal
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(f : ℝ → ℂ) (hf : MemHS f)
(hOrth : ∀ (n : ℕ),
inner
(QuantumMechanics.OneDimension.HilbertSpace.mk
⋯)
(QuantumMechanics.OneDimension.HilbertSpace.mk
hf) =
0)
(r : ℕ)
: ∫ (x : ℝ),
↑x ^ r *
(f x *
↑(Real.exp
(-x ^ 2 / (2 * Q.ξ ^ 2)))) =
0
If f is a function ℝ → ℂ satisfying MemHS f such that it is orthogonal
to all eigenfunction n then it is orthogonal to
e ^ (I c x) * e ^ (- x ^ 2 / (2 ξ^2))
for any real c.
The proof of this result relies on the expansion of e ^ (I c x)
in terms of x^r/r! and using orthogonal_power_of_mem_orthogonal
along with integrability conditions.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.orthogonal_exp_of_mem_orthogonal
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(f : ℝ → ℂ) (hf : MemHS f)
(hOrth : ∀ (n : ℕ),
inner
(QuantumMechanics.OneDimension.HilbertSpace.mk
⋯)
(QuantumMechanics.OneDimension.HilbertSpace.mk
hf) =
0)
(c : ℝ)
: ∫ (x : ℝ),
Complex.exp (Complex.I * ↑c * ↑x) *
(f x *
↑(Real.exp
(-x ^ 2 / (2 * Q.ξ ^ 2)))) =
0
If f is a function ℝ → ℂ satisfying MemHS f such that it is orthogonal
to all eigenfunction n then the fourier transform of
f (x) * e ^ (- x ^ 2 / (2 ξ^2))
is zero.
The proof of this result relies on orthogonal_exp_of_mem_orthogonal.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.fourierIntegral_zero_of_mem_orthogonal
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(f : ℝ → ℂ) (hf : MemHS f)
(hOrth : ∀ (n : ℕ),
inner
(QuantumMechanics.OneDimension.HilbertSpace.mk
⋯)
(QuantumMechanics.OneDimension.HilbertSpace.mk
hf) =
0)
: (Real.fourierIntegral fun x =>
f x *
↑(Real.exp
(-x ^ 2 / (2 * Q.ξ ^ 2)))) =
0Assuming Plancherel's theorem (which is not yet in Mathlib), the topological closure of the span of the eigenfunctions of the harmonic oscillator is the whole Hilbert space.
The proof of this result relies on fourierIntegral_zero_of_mem_orthogonal
and Plancherel's theorem which together give us that the norm of
f x * e ^ (- x^2 / (2 * ξ^2))
is zero for f orthogonal to all eigenfunctions, and hence the norm of f is zero.
Show Lean signature:
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_completeness
(Q : QuantumMechanics.OneDimension.HarmonicOscillator)
(plancherel_theorem : ∀ {f : ℝ → ℂ},
MeasureTheory.Integrable f
MeasureTheory.volume →
MeasureTheory.MemLp f 2
MeasureTheory.volume →
MeasureTheory.eLpNorm
(Real.fourierIntegral f) 2
MeasureTheory.volume =
MeasureTheory.eLpNorm f 2
MeasureTheory.volume)
: (Submodule.span ℂ
(Set.range fun n =>
QuantumMechanics.OneDimension.HilbertSpace.mk
⋯)).topologicalClosure =
⊤