leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.38k stars 307 forks source link

Define hypergeometric functions #15966

Open ocfnash opened 4 weeks ago

ocfnash commented 4 weeks ago

I think a fun 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:

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:

ocfnash commented 4 weeks ago

Also proposed on Zulip here which might be a useful place to discuss any work in this direction.

arulandu commented 1 week ago

@EdwardWatine Curious to know if you're still working on this? @ocfnash Would love to give this a shot

ocfnash commented 6 days ago

@arulandu I suggest raising this also on Zulip where most discussion takes place.