Examples: 1d Quantum Harmonic Oscillator

This module gives simple examples of how to use the QuantumMechanics.OneDimension.HarmonicOscillator API.

It is intended for experimentation and pedagogical use, and should not be imported into other modules.

To run it from the command line:

lake env lean PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Examples.lean

noncomputable def QuantumMechanics.OneDimension.HarmonicOscillator.Examples.Q : HarmonicOscillator

A concrete harmonic oscillator with m = 1, ω = 1.

Equations

• One or more equations did not get rendered due to their size.