[Merged by Bors] - feat(ModularForms/JacobiTheta): derivative of theta function #11824
Conversation
loefflerd
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
Nice work! |
leanprover-community-mathlib4-bot
added
the
merge-conflict
Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
On my system, compilation of I think merging in the long list of explicit instances would probably be judged as contravening mathlib's "house style" (especially given the conclusion of the recent zulip debate "To automate or not to automate?", where several prominent members of the community argued strongly that we should use automated systems whenever possible and tolerate some slow-down as a result). Other than that, I don't think there's much more that can be done to speed it up. May I suggest that we wait on #11980, and when that is merged, we merge this as it is? |
loefflerd
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
I tend to agree. It would be good, however, to solve the underlying problem. See also here on Zulip. |
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth. |
|
Thanks! bors merge |
github-actions
bot
added
ready-to-merge
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
This is a rewrite of
JacobiTheta/TwoVariable.lean, adding a number of new results needed for Hurwitz and Dirichlet L-series.The main addition is developing the theory of the
z-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters.We also add a number of new results about the existing
jacobiTheta2function: