Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Basic

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.

Some preliminary results about Complex.ofReal .

To be moved.

The 1d Harmonic Oscillator

The characteristic length

5 declarations

theorem

The mass $m$ is positive ( $m > 0$ ) for the 1D quantum harmonic oscillator

#m_pos

For a one-dimensional quantum harmonic oscillator, the mass $m$ is strictly positive, satisfying $0 < m$ .

theorem

The mass $m$ of the harmonic oscillator is non-negative ( $m \ge 0$ )

#m_nonneg

For a one-dimensional quantum harmonic oscillator $Q$ , the mass $m$ is non-negative, satisfying the inequality $0 \le m$ .

theorem

$\omega > 0$

#ω_pos

For a one-dimensional quantum harmonic oscillator $Q$ , the angular frequency $\omega$ is strictly positive, satisfying $0 < \omega$ .

theorem

$\omega \ge 0$

#ω_nonneg

For a one-dimensional quantum harmonic oscillator $Q$ , the angular frequency $\omega$ is non-negative, i.e., $0 \le \omega$ .

theorem

$\omega \neq 0$ for the 1D harmonic oscillator

#ω_ne_zero

For a one-dimensional quantum harmonic oscillator with angular frequency $\omega$ , the angular frequency is non-zero, i.e., $\omega \neq 0$ .

Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Basic

1d Harmonic Oscillator

Some preliminary results about Complex.ofReal .

The characteristic length

The mass mmm is positive (m>0m > 0m>0) for the 1D quantum harmonic oscillator

The mass mmm of the harmonic oscillator is non-negative (m≥0m \ge 0m≥0)

ω>0\omega > 0ω>0

ω≥0\omega \ge 0ω≥0

ω≠0\omega \neq 0ω=0 for the 1D harmonic oscillator

The mass $m$ is positive ( $m > 0$ ) for the 1D quantum harmonic oscillator

The mass $m$ of the harmonic oscillator is non-negative ( $m \ge 0$ )

$\omega > 0$

$\omega \ge 0$

$\omega \neq 0$ for the 1D harmonic oscillator