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

def

QuantumMechanics.OneDimension.HilbertSpace :
  AddSubgroup (ℝ →ₘ[MeasureTheory.volume] ℂ)
QuantumMechanics.OneDimension.HilbertSpace :
  AddSubgroup
    (ℝ →ₘ[MeasureTheory.volume] ℂ)

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

def

QuantumMechanics.OneDimension.HilbertSpace.MemHS (f : ℝ → ℂ) : Prop
QuantumMechanics.OneDimension.HilbertSpace.MemHS
  (f : ℝ → ℂ) : Prop

The proposition MemHS f for a function f : ℝ → ℂ is defined to be true if the function f can be lifted to the Hilbert space.

theorem

QuantumMechanics.OneDimension.HilbertSpace.memHS_iff {f : ℝ → ℂ} :
  MemHS f ↔
    MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume ∧
      MeasureTheory.Integrable (fun x => ‖f x‖ ^ 2) MeasureTheory.volume
QuantumMechanics.OneDimension.HilbertSpace.memHS_iff
  {f : ℝ → ℂ} :
  MemHS f ↔
    MeasureTheory.AEStronglyMeasurable f
        MeasureTheory.volume ∧
      MeasureTheory.Integrable
        (fun x => ‖f x‖ ^ 2)
        MeasureTheory.volume

A function f satisfies MemHS f if and only if it is almost everywhere strongly measurable, and square integrable.

def

QuantumMechanics.OneDimension.HilbertSpace.mk {f : ℝ → ℂ}
  (hf : MemHS f) : ↥QuantumMechanics.OneDimension.HilbertSpace
QuantumMechanics.OneDimension.HilbertSpace.mk
  {f : ℝ → ℂ} (hf : MemHS f) :
  ↥QuantumMechanics.OneDimension.HilbertSpace

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.

def

QuantumMechanics.OneDimension.HilbertSpace.parity : (ℝ → ℂ) →ₗ[ℂ] ℝ → ℂ
QuantumMechanics.OneDimension.HilbertSpace.parity :
  (ℝ → ℂ) →ₗ[ℂ] ℝ → ℂ

The parity operator is defined as linear map from ℝ → ℂ to itself, such that ψ is taken to fun x => ψ (-x).

theorem

QuantumMechanics.OneDimension.HilbertSpace.memHS_of_parity (ψ : ℝ → ℂ)
  (hψ : MemHS ψ) : MemHS (parity ψ)
QuantumMechanics.OneDimension.HilbertSpace.memHS_of_parity
  (ψ : ℝ → ℂ) (hψ : MemHS ψ) :
  MemHS (parity ψ)

The parity operator acting on a member of the Hilbert space is in Hilbert space.

1.1.3. The Schrodinger Operator

structure

QuantumMechanics.OneDimension.HarmonicOscillator : Type
QuantumMechanics.OneDimension.HarmonicOscillator :
  Type

A quantum harmonic oscillator specified by a three real parameters: the mass of the particle m, a value of Planck's constant ℏ, and an angular frequency ω. All three of these parameters are assumed to be positive.

Constructor

QuantumMechanics.OneDimension.HarmonicOscillator.mk

Fields

m : ℝ

The mass of the particle.

ℏ : ℝ

Reduced Planck's constant.

ω : ℝ

The angular frequency of the harmonic oscillator.

hℏ : 0 < self.ℏ

hω : 0 < self.ω

hm : 0 < self.m

def

QuantumMechanics.OneDimension.HarmonicOscillator.ξ
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) : ℝ
QuantumMechanics.OneDimension.HarmonicOscillator.ξ
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator) :
  ℝ

The characteristic length ξ of the harmonic oscillator is defined as √(ℏ /(m ω)).

def

QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (ψ : ℝ → ℂ) :
  ℝ → ℂ
QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator
  (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 * ψ.

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_parity
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (ψ : ℝ → ℂ) :
  Q.schrodingerOperator (parity ψ) = parity (Q.schrodingerOperator ψ)
QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_parity
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (ψ : ℝ → ℂ) :
  Q.schrodingerOperator (parity ψ) =
    parity (Q.schrodingerOperator ψ)

The Schrodinger operator commutes with the parity operator.

1.1.4. The eigenfunctions of the Schrodinger Operator

def

PhysLean.physHermite : ℕ → Polynomial ℤ
PhysLean.physHermite : ℕ → Polynomial ℤ

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.

def

QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (n : ℕ) : ℝ → ℂ
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (n : ℕ) : ℝ → ℂ

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 ξ²)).

1.1.5. Properties of the eigenfunctions

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_integrable
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (n : ℕ) :
  MeasureTheory.Integrable (Q.eigenfunction n) MeasureTheory.volume
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_integrable
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (n : ℕ) :
  MeasureTheory.Integrable
    (Q.eigenfunction n)
    MeasureTheory.volume

The eigenfunctions are integrable.

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_conj
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (n : ℕ)
  (x : ℝ) : (starRingEnd ℂ) (Q.eigenfunction n x) = Q.eigenfunction n x
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_conj
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (n : ℕ) (x : ℝ) :
  (starRingEnd ℂ) (Q.eigenfunction n x) =
    Q.eigenfunction n x

The eigenfunctions are real.

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_aeStronglyMeasurable
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (n : ℕ) :
  MeasureTheory.AEStronglyMeasurable (Q.eigenfunction n)
    MeasureTheory.volume
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_aeStronglyMeasurable
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (n : ℕ) :
  MeasureTheory.AEStronglyMeasurable
    (Q.eigenfunction n)
    MeasureTheory.volume

The eigenfunctions are almost everywhere strongly measurable.

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_square_integrable
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (n : ℕ) :
  MeasureTheory.Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2)
    MeasureTheory.volume
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_square_integrable
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (n : ℕ) :
  MeasureTheory.Integrable
    (fun x => ‖Q.eigenfunction n x‖ ^ 2)
    MeasureTheory.volume

The eigenfunctions are square integrable.

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_memHS
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (n : ℕ) :
  MemHS (Q.eigenfunction n)
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_memHS
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (n : ℕ) : MemHS (Q.eigenfunction n)

The eigenfunctions are members of the Hilbert space.

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_differentiableAt
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (x : ℝ)
  (n : ℕ) : DifferentiableAt ℝ (Q.eigenfunction n) x
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_differentiableAt
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (x : ℝ) (n : ℕ) :
  DifferentiableAt ℝ (Q.eigenfunction n) x

The eigenfunctions are differentiable.

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_orthonormal
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) :
  Orthonormal ℂ fun n => QuantumMechanics.OneDimension.HilbertSpace.mk ⋯
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_orthonormal
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator) :
  Orthonormal ℂ fun n =>
    QuantumMechanics.OneDimension.HilbertSpace.mk
      ⋯

The eigenfunctions are orthonormal within the Hilbert space.

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_parity
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (n : ℕ) :
  parity (Q.eigenfunction n) = (-1) ^ n * Q.eigenfunction n
QuantumMechanics.OneDimension.HarmonicOscillator.eigenfunction_parity
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (n : ℕ) :
  parity (Q.eigenfunction n) =
    (-1) ^ n * Q.eigenfunction n

The nth eigenfunction is an eigenfunction of the parity operator with the eigenvalue (-1) ^ n.

1.1.6. The time-independent Schrodinger Equation

def

QuantumMechanics.OneDimension.HarmonicOscillator.eigenValue
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (n : ℕ) : ℝ
QuantumMechanics.OneDimension.HarmonicOscillator.eigenValue
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (n : ℕ) : ℝ

The nth eigenvalues for a Harmonic oscillator is defined as (n + 1/2) * ℏ * ω.

theorem

QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eigenfunction
  (Q : QuantumMechanics.OneDimension.HarmonicOscillator) (n : ℕ)
  (x : ℝ) :
  Q.schrodingerOperator (Q.eigenfunction n) x =
    ↑(Q.eigenValue n) * Q.eigenfunction n x
QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eigenfunction
  (Q :
    QuantumMechanics.OneDimension.HarmonicOscillator)
  (n : ℕ) (x : ℝ) :
  Q.schrodingerOperator
      (Q.eigenfunction n) x =
    ↑(Q.eigenValue n) *
      Q.eigenfunction n x

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.

1.1.7. Completeness

theorem

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

x ^ r * e ^ (- x ^ 2 / (2 ξ^2))

the proof of this result relies on the fact that Hermite polynomials span polynomials.

theorem

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

theorem

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)))) =
    0
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)))) =
    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.

theorem

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 =
    ⊤
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 =
    ⊤

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