feat: quantum harmonic oscillator

[bjoernkjoshanssen]

I put this in "Physlib Alpha" since I haven't studied the overall fit with Physlib yet.

[github-actions]

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[jstoobysmith]

@bjoernkjoshanssen This looks good - would need to pass the linters before we could merge though. Would also recommend putting it in ./PhyslibAlpha/QuantumMechanics/HarmonicOscillator.lean

[bjoernkjoshanssen]

@bjoernkjoshanssen This looks good - would need to pass the linters before we could merge though. Would also recommend putting it in ./PhyslibAlpha/QuantumMechanics/HarmonicOscillator.lean

Thanks! Does each linter run need approval to be started? Would be nice if that was automatic.

[jstoobysmith]

@bjoernkjoshanssen It does for first-time contributors. In future PRs it will run automatically. It is also possible to run them locally (which is usually easier) details here:

https://github.com/leanprover-community/physlib/blob/master/scripts/PhyslibAlpha/README.md

[bjoernkjoshanssen]

@bjoernkjoshanssen It does for first-time contributors. In future PRs it will run automatically. It is also possible to run them locally (which is usually easier) details here:

https://github.com/leanprover-community/physlib/blob/master/scripts/PhyslibAlpha/README.md

Ah, makes sense.

[bjoernkjoshanssen]

(I got a linter error that /.lake/build/lib/lean/PhyslibAlpha.olean does not exist, but fixed it by running lake build PhyslibAlpha.)

[jstoobysmith]

To help with the linters a bit: take a look at other PhysLib files for an example copyright statement