Physlib.QuantumMechanics.OneDimension.HarmonicOscillator.Examples

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 Physlib/QuantumMechanics/OneDimension/HarmonicOscillator/Examples.lean ```

1 declaration

definition

A concrete instance of a one-dimensional quantum harmonic oscillator defined with mass $m = 1$ and angular frequency $\omega = 1$ .