Equation \phi_0(z + 1) = \phi_0(z) follows easily from periodicity of the Eisenstein series and of \Delta(z). For the second transformation law, \phi_{0}\left(-\frac{1}{z}\right) = \frac{(E_2(-1/z) E_4(-1/z) - E_6(-1/z))^{2}}{\Delta(-1/z)} = \frac{((z^2 E_2(z) - 6iz / \pi) \cdot z^4 E_4(z) - z^6 E_6(z))^{2}}{z^{12} \Delta(z)} = \frac{\left(E_2(z) E_4(z) - E_6(z) - \frac{6i}{\pi z} E_4(z)\right)^2}{\Delta(z)} = \frac{(E_2(z) E_4(z) - E_6(z))^{2} - \frac{12i}{\pi z}(E_2(z) E_4(z) - E_6(z)) E_4(z) - \frac{36}{\pi^2 z^2} E_4(z)^{2}}{\Delta(z)} = \phi_0(z) - \frac{12 i}{\pi z} \phi_{-2}(z) - \frac{36}{\pi^2 z^2} \phi_{-4}(z).

By the product formula for \Delta, \left|\frac{f(z)}{\Delta(z)}\right| = \left|\frac{\sum_{n \ge n_0} c_f(n) e^{\pi i n z}}{e^{2 \pi i z}\prod_{n \ge 1} (1 - e^{2\pi i n z})^{24}}\right| = |e^{\pi i (n_0 - 2)z}| \cdot \frac{|\sum_{n \ge n_0} c_f(n) e^{\pi i (n - n_0) z}|}{\prod_{n \ge 1} |1 - e^{2\pi i n z}|^{24}} \le e^{-\pi (n_0 - 2) \Im z} \cdot \frac{\sum_{n \ge n_0} |c_f(n)| e^{-\pi (n - n_0) \Im z}}{\prod_{n \ge 1} (1 - e^{- 2\pi n \Im z})^{24}} \le e^{-\pi (n_0 - 2) \Im z} \cdot \frac{\sum_{n \ge n_0} |c_f(n)| e^{-\pi (n - n_0) / 2}}{\prod_{n \ge 1} (1 - e^{-\pi n})^{24}} = C_f \cdot e^{-\pi (n_0 - 2) \Im z}. Here C_f = \frac{\sum_{n \ge n_0} |c_f(n)| e^{-\pi (n - n_0) / 2}}{\prod_{n \ge 1} (1 - e^{-\pi n})^{24}}. The numerator converges absolutely because of polynomial growth, and the denominator also converges; indeed it is simply e^{\pi}\cdot \Delta(i/2).

By Ramanujan's formula, E_2 E_4 - E_6 = 3E_4' = 720 \sum_{n \ge 1} n \sigma_3(n) e^{2 \pi i n z}, and (E_2(z) E_4(z) - E_6(z))^{2} = 720^{2} e^{4 \pi i z} + O(e^{5 \pi i z}). The result then follows from Lemma Lemma 8.4 with f(z) = (E_2 E_4 - E_6)^2 and n_0 = 4.

Fix n \in \N. There exists a constant C such that for all x \ge 0, |x|^n \cdot |e^{-\pi x}| \le C. In particular, for all r \ge 0 and s \ge 1, r^n \cdot e^{-\pi r/s} \le C s^n. Hence r^n \cdot \int_{1}^{\infty} e^{-2\pi s} \, e^{-\pi r /s} \, \dd{s} = \int_{1}^{\infty} e^{-2\pi s} \, \left(|r|^n \cdot e^{-\pi r /s}\right) \, \dd{s} \leq C \int_{1}^{\infty} e^{-2\pi s} \, s^n \, \dd{s}. The Gamma function is given by \Gamma(x) = \int_{0}^{\infty} e^{-u} \, u^{x-1} \, \dd{u} for all x > 0. Writing u = 2\pi s and using \Gamma(n+1) = n!, we obtain C \int_{1}^{\infty} e^{-2\pi s} \, s^n \, \dd{s} \leq C \int_{0}^{\infty} e^{-2\pi s} \, s^n \, \dd{s} = C \int_{0}^{\infty} \frac{1}{(2\pi)^{n+1}} e^{-u} \, u^n \, \dd{u} = \frac{C \cdot n!}{(2\pi)^n}. Defining C' := \frac{C \cdot n!}{(2\pi)^n} finishes the proof.

We prove the bound only for I_1(r), as the others are similar. With the change of variable z = -1 + i t for t \in [0,1], we have I_1(r) = -i \int_0^1 \phi_0\left(\frac{-1}{i t}\right) t^2 e^{-\pi i r} \cdot e^{-\pi r t} \, \dd t. With the change of variable s = 1 / t, this becomes I_1(r) = i \int_1^{\infty} \phi_0(i s) \cdot s^{-4} \cdot e^{-\pi i r} \cdot e^{-\pi r / s} \, \dd s, so |I_1(r)| \leq \int_1^{\infty} |\phi_0(i s)| \cdot s^{-4} \cdot |e^{-\pi i r}| \cdot e^{-\pi r / s} \, \dd s \le \int_1^{\infty} |\phi_0(is)| \cdot e^{-\pi r / s} \, \dd s. By Corollary Corollary 8.5, we conclude that |I_1(r)| \leq C_0 \int_1^{\infty} e^{-2\pi s} \, e^{-\pi r / s} \, \dd s.

For I_2(r), parametrize z by z = t + i for t \in [-1,0]. Then I_2(r) = \int_{-1}^0 \phi_0\left(\frac{-1}{t + 1 + i}\right) (t + 1 + i)^2 e^{\pi i r t} e^{-\pi r} \, \dd t. Since the function z \mapsto \phi_0\left(\frac{-1}{z+1}\right) (z+1)^2 is holomorphic and bounded on the contour, there exists C > 0 such that |\phi_0\left(\frac{-1}{z+1}\right) (z + 1)^2| \leq C, and therefore |I_2(r)| \le \int_{-1}^{0} C e^{-\pi r} \, \dd t = C e^{-\pi r}. The bound for I_4(r) is similar. /- source paragraph break -/ For I_6(r), parametrize z = i t for t \in [1, \infty), giving I_6(r) = 2 i \int_1^{\infty} \phi_0(i t) e^{-\pi r t} \, \dd t. Using Corollary Corollary 8.5, the absolute value is bounded by |I_6(r)| \leq 2 \int_1^{\infty} |\phi_0(i t)| e^{-\pi r t} \, \dd t \leq \frac{2C_0}{\pi} \int_1^{\infty} e^{-2\pi t} e^{-\pi r t} \, \dd t = \frac{2C_0}{\pi} \frac{e^{-\pi (r + 2)}}{r + 2}.

By Theorem Theorem 5.8, it suffices to show that the function is smooth and decays faster than any polynomial. Smoothness follows from differentiation under the integral, already formalized in mathlib. The decay follows from Lemmas Lemma 8.9 and Lemma 8.10, together with Lemma 8.8.

We recall that the Fourier transform of a Gaussian function is \mathcal{F}(e^{\pi i \|x\|^2 z})(y)=z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z}) }. Next, exchange contour integration in the z variable with Fourier transform in the x variable in the definition of a. This is justified because the corresponding double integral converges absolutely. In this way we obtain \widehat{a}(y)=\int\limits_{-1}^i\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z})}\,dz +\int\limits_{1}^i\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z})}\,dz -2\int\limits_{0}^i\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z})}\,dz +2\int\limits_{i}^{i\infty}\phi_0(z)\,z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z})}\,dz. Making the change of variables w=\frac{-1}{z}, we arrive at \widehat{a}(y)=\int\limits_{1}^i\phi_0\Big(1-\frac{1}{w-1}\Big)\,(\frac{-1}{w}+1)^2\,w^{2}\,e^{\pi i \|y\|^2 \,w}\,dw +\int\limits_{-1}^i\phi_0\Big(1-\frac{1}{w+1}\Big)\,(\frac{-1}{w}-1)^2\,w^2\,e^{\pi i \|y\|^2 \,w}\,dw -2\int\limits_{i \infty}^i\phi_0(w)\,e^{\pi i \|y\|^2 \,w}\,dw +2\int\limits_{i}^{0}\phi_0\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|y\|^2 \,w}\,dw. Since \phi_0 is 1-periodic we have \begin{aligned} \widehat{a}(y)\,=\,&\int\limits_{1}^i\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i \|y\|^2 \,z}\,dz +\int\limits_{-1}^i\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i \|y\|^2 \,z}\,dz \\ +&2\int\limits_{i}^{i\infty}\phi_0(z)\,e^{\pi i \|y\|^2 \,z}\,dz -2\int\limits_{0}^{i}\phi_0\Big(\frac{-1}{z}\Big)\,z^{2}\,e^{\pi i \|y\|^2 \,z}\,dz \\ \,=\,&a(y). \end{aligned} This finishes the proof of the proposition.

The first estimate follows from eqn:phi0-bound with z = i/t. For the second estimate, by eqn:phi0-trans-S, eqn:phi2-bound, and eqn:phi4-bound, \left|\phi_0\left(\frac{i}{t}\right)\right| \le |\phi_0(it)| + \frac{12}{\pi t} |\phi_{-2}(it)| + \frac{36}{\pi^2 t^2} |\phi_{-4}(it)| \le C_0 e^{-2 \pi t} + \frac{12}{\pi t} \cdot C_{-2} + \frac{36}{\pi^2 t^2} \cdot C_{-4} e^{2 \pi t} = O(t^{-2}e^{2 \pi t}).

Denote the right-hand side by d(r). Convergence of the integral for r > \sqrt{2} follows from Corollary Corollary 8.13. We can write d(r)=\int\limits_{-1}^{i\infty-1}\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i r^2 \,z}\,dz- 2\int\limits_{0}^{i\infty}\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\,dz +\int\limits_{1}^{i\infty+1}\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i r^2 \,z}\,dz. From eqn:phi0-trans-S we deduce that if r>\sqrt{2}, then \phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\to 0 as \Im(z)\to\infty. Therefore we can deform the paths of integration and rewrite d(r)=\int\limits_{-1}^{i}\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i r^2 \,z}\,dz +\int\limits_{i}^{i\infty}\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i r^2 \,z}\,dz -2\int\limits_{0}^{i}\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\,dz -2\int\limits_{i}^{i\infty}\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\,dz +\int\limits_{1}^{i}\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i r^2 \,z}\,dz +\int\limits_{i}^{i\infty}\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i r^2 \,z}\,dz. Now eqn:phi0-trans-S implies \phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2-2\phi_0\Big(\frac{-1}{z}\Big)\,z^2+ \phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2=2\phi_0(z), and hence d(r)=\int\limits_{-1}^{i}\phi_0\Big(\frac{-1}{z+1}\Big)\,(z+1)^2\,e^{\pi i r^2 \,z}\,dz -2\int\limits_{0}^{i}\phi_0\Big(\frac{-1}{z}\Big)\,z^2\,e^{\pi i r^2 \,z}\,dz +\int\limits_{1}^{i}\phi_0\Big(\frac{-1}{z-1}\Big)\,(z-1)^2\,e^{\pi i r^2 \,z}\,dz +2\int\limits_{i}^{i\infty}\phi_0(z)\,e^{\pi i r^2 \,z}\,dz=a(r).

Suppose that r>\sqrt{2}. Then by Proposition prop:a-double-zeros, a(r)=4i\,\sin(\pi r^2/2)^2\,\int\limits_{0}^{\infty}\phi_0(i/t)\,t^2\,e^{-\pi r^2 t}\,dt. From eqn:phi0-trans-S we obtain the asymptotic expansion \phi_0(i/t)\,t^2=\frac{36}{\pi^2}\,e^{2 \pi t}-\frac{8640}{\pi}\,t+\frac{18144}{\pi^2}+O(t^2\,e^{-2\pi t}) as t\to\infty. For r>\sqrt{2}, \int\limits_0^\infty \left(\frac{36}{\pi^2}\,e^{2 \pi t}+\frac{8640}{\pi}\,t+\frac{18144}{\pi^2}\right)\,e^{-\pi r^2 t}\,dt =\frac{36}{\pi^3\,(r^2-2)}-\frac{8640}{\pi^3\,r^4}+\frac{18144}{\pi^3\,r^2}. Therefore the claimed identity holds for r>\sqrt{2}. /- source paragraph break -/ On the other hand, the definition of a shows that a(r) is analytic in a neighborhood of [0,\infty), and the asymptotic expansion above implies that the right-hand side is also analytic there. Hence the identity holds on the whole interval [0,\infty).

These identities follow immediately from the previous proposition.

By the transformation laws of the theta-null functions, H_2|_{-2}ST = (-H_4)|_{-2}T = -H_3 H_3|_{-2}ST = (-H_3)|_{-2}T = -H_4 H_4|_{-2}ST = (-H_2)|_{-2}T = H_2. Using these identities and the level-one/level-two identities, we can rewrite \psi_I(z) as \psi_I(z) = h(z) - h|_{-2}ST(z) = 128 \frac{H_3 + H_4}{H_2^2} - 128 \frac{-H_4 + H_2}{H_3^2} = 128 \frac{H_3^2 (H_3 + H_4) - H_2^2 (H_2 - H_4)}{H_2^2 H_3^2} = 128 \frac{(H_2 + H_4)^2 (H_2 + 2 H_4) - H_2^2 (H_2 - H_4)}{H_2^2 H_3^2} = 128 \frac{H_4(5 H_2^2 + 5 H_2 H_4 + 2 H_4^2)}{ H_2^2 H_3^2} = \frac{H_4^3 (5 H_2^2 + 5 H_2 H_4 + 2 H_4^2)}{2\Delta}. Applying |_{-2}S and |_{-2}T to the expression for \psi_I proves the formulas for \psi_S and \psi_T.

The proof is similar to that of Lemma cor:phi0-bound and follows from Lemma Lemma 8.4 together with the fact that the vanishing orders of the numerators of \psi_I, \psi_T, and \psi_S at infinity are respectively 0, 0, and \frac{3}{2}.

Similar to the proof of Lemma 8.11.

We repeat the argument used in the proof of Proposition prop:a-fourier. Using the Gaussian Fourier identity and exchanging the contour integration in z with the Fourier transform in x, we get \mathcal{F}(b)(x)= \int\limits_{-1}^{i}\psi_T(z)\,z^{-4}\,e^{\pi i \|x\|^2 (\frac{-1}{z})}\,dz + \int\limits_{1}^{i}\psi_T(z)\,z^{-4}\,e^{\pi i \|x\|^2 (\frac{-1}{z})}\,dz - 2\,\int\limits_{0}^{i}\psi_I(z)\,z^{-4}\,e^{\pi i \|x\|^2 (\frac{-1}{z})}\,dz - 2\,\int\limits_{i}^{i\infty}\psi_S(z)\,z^{-4}\,e^{\pi i \|x\|^2 (\frac{-1}{z})}\,dz. With the change of variables w=\frac{-1}{z}, we arrive at \mathcal{F}(b)(x)= \int\limits_{1}^{i}\psi_T\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|x\|^2 w}\,dw + \int\limits_{-1}^{i}\psi_T\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|x\|^2 w}\,dw - 2\,\int\limits_{i\infty}^{i}\psi_I\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|x\|^2 w}\,dw - 2\,\int\limits_{i}^{0}\psi_S\Big(\frac{-1}{w}\Big)\,w^{2}\,e^{\pi i \|x\|^2 w}\,dw. Now the definitions imply \psi_T|_{-2}S=-\psi_T \psi_I|_{-2}S=\psi_S \psi_S|_{-2}S=\psi_I, so this becomes \mathcal{F}(b)(x)= \int\limits_{1}^{i}-\psi_T(z)\,e^{\pi i \|x\|^2 z}\,dz + \int\limits_{-1}^{i}-\psi_T(z)\,e^{\pi i \|x\|^2 z}\,dz + 2\,\int\limits_{i}^{i\infty}\psi_S(z)\,e^{\pi i \|x\|^2 z}\,dz + 2\,\int\limits_{0}^{i}\psi_I(z)\,e^{\pi i \|x\|^2 z}\,dw. From the definition of b, we conclude that \mathcal{F}(b)(x)=-b(x).

By eqn:psiS-define, \psi_I(it) = (it)^{-2} \psi_S\left(\frac{-1}{it}\right) = -t^{-2} \psi_S\left(\frac{i}{t}\right), and combined with eqn:psiS-bound this gives eqn:psiI-near-0. Equation eqn:psiI-near-infty follows from lemma:psi-bound.

Denote the right-hand side by c(r). By Corollary cor:psiI-near-0-infty, the integral converges for r>\sqrt{2}. Rewrite it as c(r)=\int\limits_{-1}^{i\infty-1}\psi_I(z+1)\,e^{\pi i r^2 \,z}\,dz-2\int\limits_{0}^{i\infty}\psi_I(z)\,e^{\pi i r^2 \,z}\,dz+ \int\limits_{1}^{i\infty+1}\psi_I(z-1)\,e^{\pi i r^2 \,z}\,dz. From the Fourier expansion of \psi_I, we know that \psi_I(z)=e^{-2\pi i z}+O(1) as \Im(z)\to\infty. Because r^2>2, we can deform the paths of integration and write \int\limits_{-1}^{i\infty-1}\psi_I(z+1)\,e^{\pi i r^2 \,z}\,dz= \int\limits_{-1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz+\int\limits_{i}^{i\infty}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz \int\limits_{1}^{i\infty+1}\psi_I(z-1)\,e^{\pi i r^2 \,z}\,dz= \int\limits_{-1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz+\int\limits_{i}^{i\infty}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz. Hence c(r)=\int\limits_{-1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz+\int\limits_{1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz -2\int\limits_{0}^{i}\psi_I(z)\,e^{\pi i r^2 \,z}\,dz +2\int\limits_{i}^{i\infty}(\psi_T(z)-\psi_I(z))\,e^{\pi i r^2 \,z}\,dz. Next, the functions \psi_I, \psi_T, and \psi_S satisfy \psi_T+\psi_S=\psi_I. Using this identity, we find c(r)=\int\limits_{-1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz+\int\limits_{1}^{i}\psi_T(z)\,e^{\pi i r^2 \,z}\,dz -2\int\limits_{0}^{i}\psi_I(z)\,e^{\pi i r^2 \,z}\,dz -2\int\limits_{i}^{i\infty}\psi_S(z)\,e^{\pi i r^2 \,z}\,dz=b(r).

The proof is analogous to the proof of Proposition prop:a-another-integral. First suppose that r>\sqrt{2}. Then by Proposition prop:b-double-zeros, b(r)=4i\,\sin(\pi r^2/2)^2\,\int\limits_{0}^{\infty}\psi_I(it)\,e^{-\pi r^2 t}\,dt. From the Fourier expansion of \psi_I we obtain \psi_I(it)=e^{2\pi t}+144+O(e^{-\pi t}) as t\to\infty. For r>\sqrt{2}, \int\limits_0^\infty \left(e^{2\pi t}+144\right)\,e^{-\pi r^2 t}\,dt =\frac{1}{\pi\,(r^2-2)}+\frac{144}{\pi\,r^2}. Therefore the identity holds for r>\sqrt{2}. /- source paragraph break -/ On the other hand, the definition of b shows that b(r) is analytic in a neighborhood of [0,\infty), and the asymptotic expansion above implies that the right-hand side is also analytic there. Hence the identity holds on the whole interval [0,\infty).

These identities follow immediately from the previous proposition.