Hypergeometric functions

Stream: maths

[Oliver Nash]

I was digging through some old notes recently and I was reminded that I think a really nice project would be for someone to define hypergeometric functions and prove some basic properties.

Eventually we would want the generalised ${}_pF_q$ but I think even just starting with Gauss's ${}_2F_1$ would be a great addition and probably important enough to deserve its own definition. I can imagine developing the theory along the following lines:

• define ${}_2F_1$
• prove it is analytic in the disc
• prove it satisfies the hypergeometric differential equation

Possibly most of this effort would be developing API for power series (I'm not sure just how much we have, though we do at least have some versions of the ratio test ).

More ambitious goals might be:

• prove that it can be analytically continued (e.g., taking the usual branch cut $[1, \infty)$
• derive Schwarz's list (i.e., classify parameters for which ${}_2F_1$ has finite monodromy)

[Ruben Van de Velde]

I wonder if there's a better place to document this than zulip :)

[Oliver Nash]

OK I added #15966 :)

[Johan Commelin]

@Oliver Nash should it be labeled with "good first issue"?

[Oliver Nash]

Sure, I just added it.

[EdwardW]

I did a project in undergrad in Lean, and while I am sure that I would not do this perfectly, I will still try to give this a go and try to tip my toe into contributing :grinning_face_with_smiling_eyes:

[Johan Commelin]

@EdwardW Please assign the github issue to yourself. (You can always unassign when you want to stop working on the project after some partial progress.)

[EdwardW]

Ah yes I believe I need write access for the GitHub @Johan Commelin would you be able to help with that?

[Johan Commelin]

@EdwardW What is your github login?

[EdwardW]

EdwardWatine is my username

[Johan Commelin]

@EdwardW https://github.com/leanprover-community/mathlib4/invitations

[EdwardW]

Thank you! :)

[Alvan Arulandu]

@EdwardW Curious to know if you're still working on this? Would love to give it a shot and try contributing!

[EdwardW]

@Alvan Arulandu hi :) I am still working on this, if you want I can push what I have to the branch and you can have a look and comment? Bear in mind it's a bit messy as it's a WIP. Perhaps we could develop this jointly if you wish?

[Alvan Arulandu]

@EdwardW Yes, would love to work on it jointly, so feel free to push what you have! I'm not sure that I have write access though @Johan Commelin

[Johan Commelin]

@Alvan Arulandu voila: https://github.com/leanprover-community/mathlib4/invitations

[EdwardW]

@Alvan Arulandu branch is here https://github.com/leanprover-community/mathlib4/commits/edwatine/hypergeometric-function/, fails the checks obviously but hopefully you can start to get an idea of where I'm at. I just finished a result about the Pochhammer function that may or may not be necessary, but is certainly useful and will find a place in Mathlib.
The big question is how to show convergence of the function. The best ratio test for this case that I could find is here not_summable_of_ratio_test_tendsto_gt_one, but I am also tempted by not_summable_of_ratio_norm_eventually_ge. I am not super familiar with manipulating limits (i.e. filters) so perhaps you will have more insight.

[Alvan Arulandu]

@EdwardW Thank you so much man. Will check it out

[EdwardW]

See #17448 for the PR containing first results nevermind build is failing and I don't know why all fixed :fingers_crossed: see #17455