Hydrogen atom

Stream: PhysLean

[Joseph Tooby-Smith]

I'm interested in how much can be said about the solution to the Schrödinger equation for the hydrogen atom. I'm guessing it is not yet possible to write down solution and prove it is unique, given what is currently in Mathlib.

But it may be possible to show, that for example, solutions can be split into a radial part and an angular part - and thereby split the Schrödinger equation into a radial and angular part.

I'd be interested in having anything along these lines in HepLean (which has now been renamed PhysLean).

[Winston Yin (尹維晨)]

Glad to see the rename! I think as a near term goal for mathlib to support this effort, one can develop libraries of special functions as solutions to differential equations.

[Winston Yin (尹維晨)]

You can imagine that a goal for PhysLean is to formalise famous results in undergraduate physics. Certainly that includes the spherical harmonics.

[Joseph Tooby-Smith]

Winston Yin (尹維晨) said:

Glad to see the rename! I think as a near term goal for mathlib to support this effort, one can develop libraries of special functions as solutions to differential equations.

Totally agreed!

[Joseph Tooby-Smith]

I think the basic steps for the hydrogen atom would be:

1. Write the Schrodinger equation for the hydrogen atom in Cartesian coordinates.
2. Rewrite it in terms of spherical coordinates, with a corresponding lemma showing that solutions to one leads to solutions to the other.
3. Split the spherical equation into a radial part and an angular part. Show that any solution to the full Schrodinger equation is the product of a solution from the radial and angular parts.
4. Further split the angular part into an azimuthal and polar part. Show that any solution to the full angular part is the product of a solution from the azimuthal and polar parts.
5. Use special functions as mentioned by @Winston Yin (尹維晨) , to solve the radial, azimuthal and polar parts.

I believe 1-4 would be possible now (with a bit of work).

Eventually we would want a general framework for QM and Schrodinger equation's which sit ontop of all of this.

[Kevin Buzzard]

Re 1, I think you should carefully and informally state the equation in a new thread in #**mathlib4 and ask what is needed in order to formalize the equation. That would have a lot more visibility than this channel and is clearly the place to start.

I have seen many times people coming along saying "oh mathlib should have PDEs, here is a toy example, how do we state this?" and then the experts coming along and saying "aah well you can't do d/dx but we can differentiate along an arbitary vector and you should set everything up in terms of normed spaces and not pick a basis and blah blah blah" and intimidating these people away. I think that you should not be intimidated away and should keep pressing until we have a formal statement of Schroedinger. It will be easier to take you seriously than a random newcomer who asks some questions about PDEs and then goes away again. This (stating Schroedinger) is I think one of these projects which is probably feasible given what we have, but it needs someone to drive it forwards and keep pestering until whatever fundamental obstacles there are to stating this equation are removed. Furthermore, once we have it then other people will be able to use it as a blueprint for their favourite differential equation.

[Tomas Skrivan]

One obstacle going forward will be how to compute derivatives/gradients. I have a tactic fun_trans to do it but in mathlib you can't even write the gradient of a function with type (Fin n -> R) -> R or R x R -> R(don't know how to type unicode on mobile). Yeah yeah I should use EuclideanSpace but arrow type and product type are so fundamental to the core type theory that it is hard to work without them. Internally fun_prop and fun_trans use product and arrow types to decompose complicated functions into simple ones. Once someone comes up with a predicate on functions that work only on InnerProductSpace then fun_prop will not work for it. Yes I tried using WithLp ... internally in the tactic and it got really messy and annoying. You slip once with abusing defeq and you end up with terms that just won't unify.

My solution to this would be to add additional typeclass that sits between NormedSpace and InnerProductSpace which is exactly as InnerProductSpace but requires only that the induced norm is topologically equivalent to the given norm(max norm for product and arrow types). With this weaker notion of inner product space we can define adjoint and gradient that work with product and arrow types. I tried advocating for this change/addition but didn't see any enthusiasm so I gave up. Not sure what to do about this.

And for context, the Schrodinger equation contains laplacian which can be defined as something like laplace f x = trace (fderiv (gradient f) x) i.e. you need to compute gradient for some complicated f.

[Joseph Tooby-Smith]

I realized that the hydrogen atom also has an added difficulty that the potential is not defined at zero. And thus, as a starting point, there may be easier (but still physical) examples to work with. For example planar motion in a uniform magnetic field (giving Landau levels).

@Tomas Skrivan You are implying that even if I give you a solution to the Schrodinger equation (or any other PDE) it may be difficult to check if that solution is indeed a solution?

[Tomas Skrivan]

Also I think the Schrodinger equation should be defined for a wave function with the type R -> EuclideanSpace 3 -> C(time -> space -> ...) where you can easily write the equation coordinate free.

However once you rewrite it into spherical coordinates you have to do it coordinate wise so I think it should be written in terms of a wave function with the type R -> R -> R -> R -> C(time -> radius -> latitude -> longitude -> ...) and any partial derivatives can be expressed with just deriv.

[Joseph Tooby-Smith]

Yeah! I think in general it should certainly be possible to write things in a coordinate free manner.

[Tomas Skrivan]

Yeah but if you switch to spherical coordinates then the inner product depends on the position. Therefore either you are forced to work with manifolds and covariant derivatives or write it out in coordinates.

[Tomas Skrivan]

Joseph Tooby-Smith said:

Tomas Skrivan You are implying that even if I give you a solution to the Schrodinger equation (or any other PDE) it may be difficult to check if that solution is indeed a solution?

Checking that an explicit formula is a solution is just one big exercise on computing derivatives and mathlib does not have a tactic for it. I'm working on one but the definition of InnerProductSpace is making it difficult to compute gradient.

[Tomas Skrivan]

(and I have no idea how to make this tactic work for mfderiv in case you want to go down the manifold route)

[Joseph Tooby-Smith]

Thanks for your suggestion @Kevin Buzzard . I have posted something on the mathlib channel which hopefully hits the right tone. (#mathlib4 > Stating Schrodinger's equation)

[Joseph Tooby-Smith]

Hmm annoyingly I think in the long run going down the manifold route is probably the most general way of doing things.

In particular, I believe the mathematically correct way to describe a wave function is a section of a hermitian line bundle, and there are 'physical' examples where this really matters - my first ever paper actually happened to be related to this very topic :). A particular example is the case of a Dirac monopole (which is related to the concept of a Dirac string).

But maybe sticking with fderiv and gradient for now is the best idea.

[Tomas Skrivan]

Joseph Tooby-Smith said:

But maybe sticking with fderiv and gradient for now is the best idea.

I think so too and not only because of technical reasons but social ones. As Kevin mentioned, we already struggle with keeping people involved so we should keep it a bit closer to the math people are used to. Many many parts of physics and applied math don't use the language of differential geometry so I think forcing people to learn what "modelWithCornersEuclideanHalfSpace" before they can do the most basic stuff is not a good idea.

[Tomas Skrivan]

It is already crazy that people have to learn that vector space is addcommgroup+module ...

[Joseph Tooby-Smith]

Yeah, ok I agree.

I think an ideal case would be something along the following lines:

Since one day it would be nice to have things like dirac monopoles, the general framework (e.g. in terms of mfderiv) is needed.
But this should be related to, in the cases where it can be, to a specific framework (e.g. in terms of fderiv and gradient) which is easier to understand and closer to what the average physicist is use too. Those who don't care about the general framework won't need to use it or even know of its existence.

[Winston Yin (尹維晨)]

I think it's a great stress test of Lean/mathlib to formalise the hydrogen atom as a PDE problem first. Have you thought about generality on the physics side, namely that the Schrödinger equation is a special case of the eigenvalue problem of a Hermitian operator on a Hilbert space? For example, there are some subtleties with the Laplacian when you're dealing with infinite potential walls in tunnelling or particle in a box problems. Hilbert spaces are actually too restrictive, since we want to be able to treat non-integrable functions/distributions as solutions (e.g. plane waves) from which integrable solutions are built.

[Tyler Josephson ⚛️]

Quantum chemists would appreciate branching off from this into theories like Hartree Fock, LDA, and DFT. But exact solutions for the hydrogen atom make the most sense to do first, I think.

[Joseph Tooby-Smith]

@Winston Yin (尹維晨) Yeah, at some point all of this will need to be handled properly. Which may lead to difficulties - but for now getting some examples done is, I think the way to go.

[Joseph Tooby-Smith]

Joseph Tooby-Smith said:

I think the basic steps for the hydrogen atom would be:

1. Write the Schrodinger equation for the hydrogen atom in Cartesian coordinates.
2. Rewrite it in terms of spherical coordinates, with a corresponding lemma showing that solutions to one leads to solutions to the other.
3. Split the spherical equation into a radial part and an angular part. Show that any solution to the full Schrodinger equation is the product of a solution from the radial and angular parts.
4. Further split the angular part into an azimuthal and polar part. Show that any solution to the full angular part is the product of a solution from the azimuthal and polar parts.
5. Use special functions as mentioned by Winston Yin (尹維晨) , to solve the radial, azimuthal and polar parts.

I believe 1-4 would be possible now (with a bit of work).

Eventually we would want a general framework for QM and Schrodinger equation's which sit ontop of all of this.

I was a bit stupid in part of this message, you don't need to do the Show that any solution.... parts, you just need to show completeness of solutions at the end, once you have them.

[Tyler Josephson ⚛️]

Tyler Josephson ⚛️ said:

Quantum chemists would appreciate branching off from this into theories like Hartree Fock, LDA, and DFT. But exact solutions for the hydrogen atom make the most sense to do first, I think.

If any of y’all wanted to pursue this more deeply, I’d be happy to help write proposals to get funding for this sort of thing. I think “Formally verified quantum chemistry” is a kind of project that would get a lot of traction at various funding agencies (though who knows about the future of science funding in the US right now).

[Winston Yin (尹維晨)]

I'm likely completely overloaded until at least June, so I can only give my moral support at the moment.

[Joseph Tooby-Smith]

My knowledge of things like Hartree Fock, LDA and DFT isn't great. But I'd be interested in learning what you have in mind there Tyler. Maybe we could chat at some point?

[Joseph Tooby-Smith]

Regarding the more basics of QM I created a 'tracking issue' here:

https://github.com/HEPLean/PhysLean/issues/346

Anyone should feel free to add more details, examples, references etc, or attempt to do any of the points.

[Alex Meiburg]

I've done stuff with HF (have a paper on it, at least) .. and, to a lesser degree, DFT. I would be interested in collaborating on some 'verified quantum chemistry'