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 eigenfunctions and eigenvalues.
TODO #
- Show that Schrodinger operator is linear.
Some preliminary results about Complex.ofReal . #
To be moved.
The 1d Harmonic Oscillator
The characteristic length #
The characteristic length ξ
of the harmonic oscillator is defined
as √(ℏ /(m ω))
.
Instances For
The momentum operator is defined as the map from ℝ → ℂ
to ℝ → ℂ
taking
ψ
to - i ℏ ψ'
.
The notation Pᵒᵖ
can be used for the momentum operator.
Equations
Instances For
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ᵒᵖ")
Instances For
The position operator is defined as the map from ℝ → ℂ
to ℝ → ℂ
taking
ψ
to x ψ'
.
The notation Xᵒᵖ
can be used for the momentum operator.
Equations
Instances For
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ᵒᵖ")
Instances For
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
Instances For
The schrodinger operator written in terms of ξ
.
The Schrodinger operator commutes with the parity operator.