Commit 2024-04-08 13:15 3576301e

feat(ModularForms/JacobiTheta): derivative of theta function (#11824) 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.