Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Define hypergeometric functions #15966

Open
ocfnash opened this issue Aug 19, 2024 · 3 comments
Open

Define hypergeometric functions #15966

ocfnash opened this issue Aug 19, 2024 · 3 comments
Assignees
Labels
enhancement New feature or request good first issue Good for newcomers help-wanted The author needs attention to resolve issues t-analysis Analysis (normed *, calculus)

Comments

@ocfnash
Copy link
Contributor

ocfnash commented Aug 19, 2024

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:

  • 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 (taking the usual branch cut $$[1, \infty)$$)
  • derive Schwarz's list (i.e., classify parameters for which $${}_2F_1$$ has finite monodromy)
@ocfnash ocfnash added enhancement New feature or request help-wanted The author needs attention to resolve issues t-analysis Analysis (normed *, calculus) labels Aug 19, 2024
@ocfnash
Copy link
Contributor Author

ocfnash commented Aug 19, 2024

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

@ocfnash ocfnash added the good first issue Good for newcomers label Aug 19, 2024
@EdwardWatine EdwardWatine self-assigned this Sep 3, 2024
@arulandu
Copy link
Collaborator

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

@ocfnash
Copy link
Contributor Author

ocfnash commented Sep 10, 2024

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

EdwardWatine added a commit that referenced this issue Oct 5, 2024
…y\Polynomial\Pochhammer): add the ordinaryHyperGeometricSeries and some related theorems

Add the definition of the ordinary hypergeometric series, and show that its radius is one. Part of this requires an additional theorem about ascPochhammer, which can be found in the ascPochhammer file. Closely follows the exponential series definition.

#15966
mathlib-bors bot pushed a commit that referenced this issue Oct 17, 2024
Add the definition of the ordinary hypergeometric series, and show that its radius is one. Part of this requires an additional theorem about ascPochhammer, which is found in the Pochhammer file. Closely follows the exponential series definition.

#15966



Co-authored-by: Alvan Caleb Arulandu <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request good first issue Good for newcomers help-wanted The author needs attention to resolve issues t-analysis Analysis (normed *, calculus)
Projects
None yet
Development

No branches or pull requests

3 participants