1d Harmonic Oscillator

The quantum harmonic oscillator in 1d. This file contains

• the definition of the Schrodinger operator
• the definition of eigenfunctions and eigenvalues of the Schrodinger operator in terms of Hermite polynomials
• proof that eigenfunctions and eigenvalues are indeed egienfunctions and eigenvalues.

TODO

• Show that Schrodinger operator is linear.

Some preliminary results about Complex.ofReal .

To be moved.

theorem Complex.ofReal_hasDerivAt {x : ℝ} : HasDerivAt ofReal 1 x

@[simp]

theorem Complex.deriv_ofReal {x : ℝ} : deriv ofReal x = 1

theorem Complex.differentiableAt_ofReal {x : ℝ} : DifferentiableAt ℝ ofReal x

The 1d Harmonic Oscillator

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

• 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

@[simp]

theorem QuantumMechanics.OneDimension.HarmonicOscillator.m_mul_ω_div_two_ℏ_pos (Q : HarmonicOscillator) : 0 < Q.m * Q.ω / (2 * Q.ℏ)

@[simp]

theorem QuantumMechanics.OneDimension.HarmonicOscillator.m_mul_ω_div_ℏ_pos (Q : HarmonicOscillator) : 0 < Q.m * Q.ω / Q.ℏ

theorem QuantumMechanics.OneDimension.HarmonicOscillator.m_ne_zero (Q : HarmonicOscillator) : Q.m ≠ 0

theorem QuantumMechanics.OneDimension.HarmonicOscillator.ℏ_ne_zero (Q : HarmonicOscillator) : Q.ℏ ≠ 0

The characteristic length

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

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

Equations

• Q.ξ = √(Q.ℏ / (Q.m * Q.ω))

theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_nonneg (Q : HarmonicOscillator) : 0 ≤ Q.ξ

@[simp]

theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_pos (Q : HarmonicOscillator) : 0 < Q.ξ

@[simp]

theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_ne_zero (Q : HarmonicOscillator) : Q.ξ ≠ 0

theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_sq (Q : HarmonicOscillator) : Q.ξ ^ 2 = Q.ℏ / (Q.m * Q.ω)

@[simp]

theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_abs (Q : HarmonicOscillator) : |Q.ξ| = Q.ξ

theorem QuantumMechanics.OneDimension.HarmonicOscillator.one_over_ξ (Q : HarmonicOscillator) : 1 / Q.ξ = √(Q.m * Q.ω / Q.ℏ)

theorem QuantumMechanics.OneDimension.HarmonicOscillator.ξ_inverse (Q : HarmonicOscillator) : Q.ξ⁻¹ = √(Q.m * Q.ω / Q.ℏ)

theorem QuantumMechanics.OneDimension.HarmonicOscillator.one_over_ξ_sq (Q : HarmonicOscillator) : (1 / Q.ξ) ^ 2 = Q.m * Q.ω / Q.ℏ

noncomputable def QuantumMechanics.OneDimension.HarmonicOscillator.momentumOperator (Q : HarmonicOscillator) (ψ : ℝ → ℂ) : ℝ → ℂ

The momentum operator is defined as the map from ℝ → ℂ to ℝ → ℂ taking ψ to - i ℏ ψ'.

The notation Pᵒᵖ can be used for the momentum operator.

Equations

• Q.momentumOperator ψ x = -Complex.I * ↑Q.ℏ * deriv ψ x

def QuantumMechanics.OneDimension.HarmonicOscillator.«termPᵒᵖ» : Lean.ParserDescr

The momentum operator is defined as the map from ℝ → ℂ to ℝ → ℂ taking ψ to - i ℏ ψ'.

The notation Pᵒᵖ can be used for the momentum operator.

Equations

• QuantumMechanics.OneDimension.HarmonicOscillator.«termPᵒᵖ» = Lean.ParserDescr.node `QuantumMechanics.OneDimension.HarmonicOscillator.«termPᵒᵖ» 1024 (Lean.ParserDescr.symbol "Pᵒᵖ")

noncomputable def QuantumMechanics.OneDimension.HarmonicOscillator.positionOperator (ψ : ℝ → ℂ) : ℝ → ℂ

The position operator is defined as the map from ℝ → ℂ to ℝ → ℂ taking ψ to x ψ'.

The notation Xᵒᵖ can be used for the momentum operator.

Equations

• QuantumMechanics.OneDimension.HarmonicOscillator.positionOperator ψ x = ↑x * ψ x

def QuantumMechanics.OneDimension.HarmonicOscillator.«termXᵒᵖ» : Lean.ParserDescr

The position operator is defined as the map from ℝ → ℂ to ℝ → ℂ taking ψ to x ψ'.

The notation Xᵒᵖ can be used for the momentum operator.

Equations

• QuantumMechanics.OneDimension.HarmonicOscillator.«termXᵒᵖ» = Lean.ParserDescr.node `QuantumMechanics.OneDimension.HarmonicOscillator.«termXᵒᵖ» 1024 (Lean.ParserDescr.symbol "Xᵒᵖ")

noncomputable def QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator (Q : 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 * ψ.

Equations

• Q.schrodingerOperator ψ x = -↑Q.ℏ ^ 2 / (2 * ↑Q.m) * deriv (deriv ψ) x + 1 / 2 * ↑Q.m * ↑Q.ω ^ 2 * ↑x ^ 2 * ψ x

theorem QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eq (Q : HarmonicOscillator) (ψ : ℝ → ℂ) : Q.schrodingerOperator ψ = (-Q.ℏ ^ 2 / (2 * Q.m)) • deriv (deriv ψ) + (1 / 2 * Q.m * Q.ω ^ 2) • ((fun (x : ℝ) => ↑x ^ 2) * ψ)

theorem QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eq_ξ (Q : HarmonicOscillator) (ψ : ℝ → ℂ) : Q.schrodingerOperator ψ = fun (x : ℝ) => ↑Q.ℏ ^ 2 / (2 * ↑Q.m) * (-deriv (deriv ψ) x + (1 / ↑Q.ξ ^ 2) ^ 2 * ↑x ^ 2 * ψ x)

The schrodinger operator written in terms of ξ.

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

The Schrodinger operator commutes with the parity operator.