Curated notes for Harmonic Oscillator

Stream: PhysLean

[Joseph Tooby-Smith]

So the formalization of the quantum harmonic oscillator is now in PhysLean. One of the things I'm currently exploring is 'curated notes', and I have made one for the harmonic oscillator here.

The motivation behind these notes is two fold:

• Firstly, I hope they give the new or experienced Lean user an idea of the (story of the) formalization without them having to work through every definition and theorem.
• Secondly, I hope (and maybe this is unfounded) that they will also be useful for physicists not initiated in Lean who want to learn about a specific topic.

I also hope that they can be used to in a sense "advertise" the project more generally.

The notes are made directly from the Lean code using doc-strings with some additional text surrounding this.

Any feedback would be greatly appreciated.

[Yakov Pechersky]

Looking at the lean code for lemma 2.3, https://heplean.com/CuratedNotes/HarmonicOscillator.html#decl-2.3, I would suggest using structured goals so that you don't have two exacts right after each other. and/or using suffices

[Yakov Pechersky]

And perhaps for physlean or just this file, it makes sense to have a CoeFun for polynomial so that you don't have to have a separate HermiteFun def. Or have simp lemmas that describe its ring hom nature.

[Yakov Pechersky]

Additionally, I think if you're trying to get across clarity in the lean code, for example that the eigenfunction is real, it might be better to not squeeze the simps but to have a plain terminal simp without specifying lemmas.

[Yakov Pechersky]

Similarly, proofs like this are shorter and at the same time, I think clearer:

lemma eigenfunction_aeStronglyMeasurable (n : ℕ) :
    MeasureTheory.AEStronglyMeasurable (Q.eigenfunction n) :=
  (Q.eigenfunction_integrable n).aestronglyMeasurable

[Joseph Tooby-Smith]

Thanks @Yakov Pechersky ! I agree with all of these points.
Though weirdly the terminal simp of eigenfunction_conj doesn't actually work if turned into a plain simp (I think other simp lemmas get in the way). I'm going to have a go to see if I can get something working regarding the CoeFun .

Let me add in passing, here that the 'curated note' is actually made from a number of different files (and select theorems and definitions therein) within PhysLean.

[Yakov Pechersky]

Please leave a note here about which simp lemmas get in the way! I do this by doing simp? and remarking which ones get mentioned that I don't want. It's possible we have a coercion/cast lemma pointing the "wrong" way.

[Joseph Tooby-Smith]

It's Complex.ofReal_exp that gets in the way, because it overrides Complex.conj_ofReal.

Here is a mwe

Code

import Mathlib

example (x : ℝ) : (starRingEnd ℂ) (Complex.ofReal (Real.exp (x))) =
    (Complex.ofReal (Real.exp (x))) := by
  simp  -- does not work
  -- simp only [Complex.conj_ofReal] -- works

[Yakov Pechersky]

Perhaps in this file, you want to turn off that lemma, since you're almost never going to be discussing Complex.exp.

import Mathlib

example (x : ℝ) : (starRingEnd ℂ) (Complex.ofReal (Real.exp (x))) =
    (Complex.ofReal (Real.exp (x))) := by
  simp [-Complex.ofReal_exp]

-- or

local attribute [-simp] Complex.ofReal_exp

example (x : ℝ) : (starRingEnd ℂ) (Complex.ofReal (Real.exp (x))) =
    (Complex.ofReal (Real.exp (x))) := by
  simp

[Kevin Buzzard]

docs#Rat.cast_neg is a simp lemma which pushes the coercion inwards under a unary operator. I don't know what the conventions are in general but this makes me think that Complex.ofReal_exp might be going in the right direction as far as mathlib is concerned, and perhaps what you want is another simp lemma saying (starRingEnd ℂ) (Complex.exp z) = Complex.exp (starRingEnd ℂ z) to make simp confluent again.

[Kevin Buzzard]

@[simp] lemma foo (z : ℂ) : (starRingEnd ℂ) (Complex.exp z) = Complex.exp (starRingEnd ℂ z) := by
  sorry

example (x : ℝ) : (starRingEnd ℂ) (Complex.ofReal (Real.exp (x))) =
    (Complex.ofReal (Real.exp (x))) := by
  simp -- now works

I've never worked in this part of the library and can't guarantee that this simp lemma is OK but if it makes the simp set confluent then that sounds like good evidence that it should be there.

[Yakov Pechersky]

import Mathlib

@[simp]
lemma kevin (z : ℂ) : (starRingEnd ℂ) (Complex.exp z) = Complex.exp (starRingEnd ℂ z) := by
  simp -- uh-oh, simpNF linter will complain

example (x : ℝ) : (starRingEnd ℂ) (Complex.ofReal (Real.exp (x))) =
    (Complex.ofReal (Real.exp (x))) := by
  simp

[Joseph Tooby-Smith]

Hmm, yeah seems like Complex.exp_conj and Complex.ofReal_exp act against each other here.

[Kevin Buzzard]

So perhaps one can argue that docs#Complex.exp_conj is backwards (i.e. should be a simp lemma the other way around). Searching for it in mathlib I see 7 rw [← exp_conj] and only 4 rw [exp_conj] (although there is more than one lemma called exp_conj) so you might want to raise this issue in #mathlib4 and see if people think changing the direction is a good idea. You could of course just try changing the type of the lemma in mathlib and seeing what breaks.

[Yakov Pechersky]

My thought is that the only things that exp foo could be simplied on are exp 0 and exp over ring expressions. On which conj would operate as well into the obvious forms. And conj can operate on more expressions than just ring expressions, including re and im. So exp should stay on the outside.

[Alex Meiburg]

Nice! With this it should be pretty immediate to prove, e.g. the spectrum of the QHO, or to show the Virial theorem for it, right?

[Joseph Tooby-Smith]

It should be! The spectrum is already there in the form of the TISE, but not formally defined as such.
If anyone wants to have a go at the Virial theorem and push it to PhysLean please do!

[Joseph Tooby-Smith]

As an aside: For these ‘curated notes’, I have added drop down menus for each definition and theorem which allows one to easily generate a GitHub issue related to that definition or theorem. In particular it allows one to suggest improvements to the name, lean code or doc-string.

[Joseph Tooby-Smith]

These curated notes are now written in Verso: e.g.

https://notes.physlean.com/Quantum-Mechanics/Quantum-Harmonic-Oscillator/#QHO

My aim is that these notes is that they will expand to cover other areas in PhysLean, and in conjunction with PhysLean (though PhysLean itself will always be the priority). In particular one area that particularly needs covering is: The Lorentz group.

If anyone wants to help with any of this side of things let me know!

[Matteo Cipollina]

I'd be happy to work on curated notes for the Lorentz Group since I'm already working on PRs to develop the Relativity folder in PhysLean

[Joseph Tooby-Smith]

@Matteo Cipollina This would be helpful :)