The time-independent Schrodinger equation

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

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

Equations

• Q.eigenValue n = (↑n + 1 / 2) * Q.ℏ * Q.ω

Derivatives of the eigenfunctions

theorem QuantumMechanics.OneDimension.HarmonicOscillator.deriv_eigenfunction_zero (Q : HarmonicOscillator) : deriv (Q.eigenfunction 0) = ↑(-1 / Q.ξ ^ 2) • Complex.ofReal * Q.eigenfunction 0

theorem QuantumMechanics.OneDimension.HarmonicOscillator.deriv_eigenfunction_zero' (Q : HarmonicOscillator) : deriv (Q.eigenfunction 0) = (-↑√2 / (2 * ↑Q.ξ)) • Q.eigenfunction 1

theorem QuantumMechanics.OneDimension.HarmonicOscillator.deriv_physHermite_characteristic_length (Q : HarmonicOscillator) (n : ℕ) : (deriv fun (x : ℝ) => ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ))) = fun (x : ℝ) => ↑(1 / Q.ξ) * 2 * ↑n * ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite (n - 1))) (x / Q.ξ))

theorem QuantumMechanics.OneDimension.HarmonicOscillator.deriv_eigenfunction_succ (Q : HarmonicOscillator) (n : ℕ) : deriv (Q.eigenfunction (n + 1)) = fun (x : ℝ) => ↑(1 / √(2 ^ (n + 1) * ↑(n + 1).factorial) * (1 / Q.ξ)) • ((2 * (↑n + 1) * ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ)) - ↑x / ↑Q.ξ * ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite (n + 1))) (x / Q.ξ))) * Q.eigenfunction 0 x)

Second derivatives of the eigenfunctions.

theorem QuantumMechanics.OneDimension.HarmonicOscillator.deriv_deriv_eigenfunction_zero (Q : HarmonicOscillator) (x : ℝ) : deriv (deriv (Q.eigenfunction 0)) x = -1 / ↑Q.ξ ^ 2 * (1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction 0 x

theorem QuantumMechanics.OneDimension.HarmonicOscillator.deriv_deriv_eigenfunction_succ (Q : HarmonicOscillator) (n : ℕ) (x : ℝ) : deriv (fun (x : ℝ) => deriv (Q.eigenfunction (n + 1)) x) x = ↑(1 / √(2 ^ (n + 1) * ↑(n + 1).factorial) * (1 / Q.ξ)) * ((2 * (↑n + 1) * deriv (fun (x : ℝ) => ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ))) x + -(1 / ↑Q.ξ ^ 2) * (4 * (↑n + 1) * ↑x) * ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite n)) (x / Q.ξ)) + -(1 / ↑Q.ξ) * (1 + -(1 / ↑Q.ξ ^ 2) * ↑x ^ 2) * ↑((fun (x : ℝ) => (Polynomial.aeval x) (PhysLean.physHermite (n + 1))) (x / Q.ξ))) * Q.eigenfunction 0 x)

theorem QuantumMechanics.OneDimension.HarmonicOscillator.deriv_deriv_eigenfunction (Q : HarmonicOscillator) (n : ℕ) (x : ℝ) : deriv (fun (x : ℝ) => deriv (Q.eigenfunction n) x) x = -1 / ↑Q.ξ ^ 2 * (2 * ↑n + 1 + -1 / ↑Q.ξ ^ 2 * ↑x ^ 2) * Q.eigenfunction n x

Application of the schrodingerOperator

theorem QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eigenfunction (Q : 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 scillator,

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.