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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat (number_theory/modular_forms): holomorphy of the Jacobi theta function #18631

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat (number_theory/modular_forms): holomorphy of the Jacobi theta function #18631

wants to merge 13 commits into from

Conversation

loefflerd
Copy link
Collaborator

Show that the Jacobi theta function is holomorphic on the upper half-plane, with exponential decay at infinity.

Open in Gitpod

CBirkbeck
CBirkbeck reviewed Mar 22, 2023
View reviewed changes
src/geometry/manifold/mfderiv.lean Outdated Show resolved Hide resolved
src/geometry/manifold/mfderiv.lean Outdated Show resolved Hide resolved
@loefflerd loefflerd marked this pull request as ready for review March 22, 2023 18:10
@loefflerd loefflerd added the awaiting-review The author would like community review of the PR label Mar 27, 2023
@loefflerd
Copy link
Collaborator Author

I realised as an afterthought that, now we're using the general result on differentiability of uniformly-convergent sums, there's no longer any need to expose the internals of jacobi_theta_unif_summable. This shortens the proof somewhat and reduces clutter.

@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 29, 2023
@loefflerd loefflerd added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 29, 2023
@sgouezel
Copy link
Collaborator

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 30, 2023
bors bot pushed a commit that referenced this pull request Mar 30, 2023
@loefflerd
feat (number_theory/modular_forms): holomorphy of the Jacobi theta fu…
fe44cd3 
…nction (#18631)

Show that the Jacobi theta function is holomorphic on the upper half-plane, with exponential decay at infinity.
@bors
Copy link

bors bot commented Mar 30, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat (number_theory/modular_forms): holomorphy of the Jacobi theta function [Merged by Bors] - feat (number_theory/modular_forms): holomorphy of the Jacobi theta function Mar 30, 2023
@bors bors bot closed this Mar 30, 2023
@bors bors bot deleted the DL_jacobi_theta_holo branch March 30, 2023 07:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

@CBirkbeck CBirkbeck CBirkbeck left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@loefflerd @sgouezel @CBirkbeck