Definitions/Def_ModularCurve_SiegelFunction.lean

For a natural number N, integers r,s and a complex number z, ModularCurve.siegelFun N r s z is the explicit product -e^{\pi i s(r-N)/N^{2}}\; e^{\pi i\left((r/N)^{2}-r/N+1/6\right)z}\;\bigl(1-q_a\bigr)\prod_{n\ge 0}\bigl(1-q^{\,n+1}q_a\bigr)\bigl(1-q^{\,n+1}q_a^{-1}\bigr), where q=e^{2\pi i z} and q_a=e^{2\pi i (rz+s)/N}, and where the inner power q^{n+1} is literally e^{2\pi i z} raised to the natural-number exponent n+1. Writing a=(a_1,a_2)=(r/N,s/N), the first exponential is -e^{2\pi i a_2(a_1-1)/2}, the second is q^{B_2(a_1)/2} with B_2(x)=x^{2}-x+1/6 the second Bernoulli polynomial, and q_a=e^{2\pi i(a_1z+a_2)}; thus the definition is the classical Siegel function g_a in the Kubert–Lang normalisation, indexed by a pair of integers rather than by a reduced residue pair, so r and s are not taken modulo N.

The function is defined for every z\in\mathbb{C}, with no hypothesis on N, r, s; the infinite product is Mathlib's unconditional ∏', which agrees with the usual limit exactly when the factors form a multipliable family, as happens for z in the upper half-plane, where the product converges absolutely. Since the divisions are field divisions, the case N=0 degenerates: the factor 1-e^{2\pi i(rz+s)/N} becomes 1-e^{0}=0, so siegelFun 0 r s z = 0 for all r,s,z. The companion declaration ModularCurve.siegelFun_def records the defining identity as an equation available for rewriting. No analytic property (modularity of g_a^{12N}, the relation to Klein forms and \eta^2, absence of zeros and poles on the upper half-plane) is asserted here; only the q-product itself is fixed.