Sphere Packing in Lean

7 Fourier eigenfunctions with double zeroes at lattice points

In this section we construct two radial Schwartz functions \(a,b:\mathbb {R}^8\to i\mathbb {R}\) such that

\begin{align} \mathcal{F}(a)& =a\label{eqn:a-fourier}\\ \mathcal{F}(b)& =-b\label{eqn:b-fourier} \end{align}

which double zeroes at all \(\Lambda _8\)-vectors of length greater than \(\sqrt{2}\). Recall that each vector of \(\Lambda _8\) has length \(\sqrt{2n}\) for some \(n\in \mathbb {N}_{\geq 0}\). We define \(a\) and \(b\) so that their values are purely imaginary because this simplifies some of our computations. We will show in Section 8 that an appropriate linear combination of functions \(a\) and \(b\) satisfies conditions 68.

Both of the functions will be defined via certain integrals of (quasi)modular forms. Then the eigenfunction property mainly follows from the Poisson summation formula (Theorem 4.7) and the transformation laws of (quasi)modular forms. To apply Theorem 4.7, we will show that \(a(x)\) and \(b(x)\) are Schwartz functions, and this can be proved by verifying fast decay of the integrals.

First, we will define function \(a\). To this end we consider the following functions:

Definition 7.1
\begin{align} \phi _{-4} & := \frac{E_4^2}{\Delta } \label{eqn: def phi4} \\ \phi _{-2} & := \frac{E_4(E_2 E_4 - E_6)}{\Delta } \label{eqn: def phi2} \\ \phi _{0} & := \frac{(E_2 E_4 - E_6)^2}{\Delta } \label{eqn: def phi0} \end{align}

The function \(\phi _0(z)\) is not modular; however, it satisfies the following transformation rules:

We have

\begin{align} \phi _0(z + 1) & = \phi _0(z) \label{eqn:phi0-trans-T} \\ \phi _0\left(-\frac{1}{z}\right) & = \phi _0(z)-\frac{12i}{\pi }\, \frac{1}{z}\, \phi _{-2}(z)-\frac{36}{\pi ^2}\, \frac{1}{z^2}\, \phi _{-4}(z).\label{eqn:phi0-trans-S} \end{align}
Proof

118 easily follows from periodicity of Eisenstein series and \(\Delta (z)\). For 119,

\begin{align} \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). \end{align}

For our formalization, we choose rectangular contours for the first and the second integral, and write it as follows.

Definition 7.3

Define \(a_{\mathrm{rad}} : \mathbb {R}\to \mathbb {C}\) by

\begin{align} \label{eqn:a-rad-definition} a_\mathrm{rad}(r) := I_1(r) + I_2(r) + I_3(r) + I_4(r) + I_5(r) + I_6(r) \end{align}

where

\begin{align} I_1(r) & := \int _{-1}^{-1 + i} \phi _0 \left(\frac{-1}{z+1}\right) (z + 1)^2 e^{\pi i r z} \mathrm{d}z \label{eqn:a-I1} \\ I_2(r) & := \int _{-1 + i}^{i} \phi _0 \left(\frac{-1}{z+1}\right) (z + 1)^2 e^{\pi i r z} \mathrm{d}z \label{eqn:a-I2} \\ I_3(r) & := \int _{1}^{1 + i} \phi _0 \left(\frac{-1}{z-1}\right) (z - 1)^2 e^{\pi i r z} \mathrm{d}z \label{eqn:a-I3} \\ I_4(r) & := \int _{1 + i}^{i} \phi _0 \left(\frac{-1}{z-1}\right) (z - 1)^2 e^{\pi i r z} \mathrm{d}z \label{eqn:a-I4} \\ I_5(r) & := -2 \int _{0}^{i} \phi _0 \left(\frac{-1}{z}\right) z^2 e^{\pi i r z} \mathrm{d}z \label{eqn:a-I5} \\ I_6(r) & := 2 \int _{i}^{i\infty } \phi _0(z) e^{\pi i r z} \mathrm{d}z \label{eqn:a-I6} \end{align}

Here all the contours are chosen to be straight line segments. Now, define \(a(x) := a_{\mathrm{rad}}(\| x\| ^2)\) for \(x \in \mathbb {R}^8\).

In the original paper, the integrals \(I_1\) and \(I_2\) are combined, as well as \(I_3\) and \(I_4\). We choose to write them separately to simplify the formalization.

Now we prove that \(a\) satisfies condition 113. The following lemma will be used to prove Schwartzness of \(a\) and \(b\).

Let \(f(z)\) be a holomorphic function with a Fourier expansion

\begin{equation} f(z) = \sum _{n \ge n_0} c_f(n) e^{\pi i n z} \end{equation}
132

with \(c_f(n_0) \ne 0\). Assume that \(c_f(n)\) has a polynomial growth, i.e. \(|c_f(n)| = O(n^k)\) for some \(k \in \mathbb {N}\). Then there exists a constant \(C_f {\gt} 0\) such that

\begin{equation} \left|\frac{f(z)}{\Delta (z)}\right| \le C_f e^{-\pi (n_0 - 2) \Im z} \end{equation}
133

for all \(z\) with \(\Im z {\gt} 1/2\).

When \(f(z)\) is a (quasi)modular form, we can take \(k\) to be the weight of \(f\).

Proof

By the product formula 12,

\begin{align} \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} \end{align}

where

\begin{equation} 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}}. \end{equation}
139

Note that the summation in the numerator converges absolutely because of polynomial growth. The denominator also converges, which is simply \(e^{\pi } \cdot \Delta (i/2)\).

As corollaries, we have the following bound for \(\phi _0\), \(\phi _{-2}\), and \(\phi _{-4}\).

There exists a constant \(C_0 {\gt} 0\) such that

\begin{equation} \label{eqn:phi0-bound} |\phi _0(z)| \le C_0 e^{-2 \pi \Im z} \end{equation}
140

for all \(z\) with \(\Im z {\gt} 1/2\).

Proof

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

\begin{equation} (E_2(z) E_4(z) - E_6(z))^{2} = 720^{2} e^{4 \pi i z} + O(e^{5 \pi i z}). \notag \end{equation}
141

Then the result follows from Lemma 7.4 with \(f(z) = (E_2 E_4 - E_6)^2\) and \(n_0 = 4\).

Corollary 7.6

There exists a constant \(C_{-2} {\gt} 0\) such that

\begin{equation} \label{eqn:phi2-bound} |\phi _{-2}(z)| \le C_{-2} \end{equation}
141

for all \(z\) with \(\Im z {\gt} 1/2\).

Corollary 7.7

There exists a constant \(C_{-4} {\gt} 0\) such that

\begin{equation} \label{eqn:phi4-bound} |\phi _{-4}(z)| \le C_{-4} e^{2 \pi \Im z} \end{equation}
142

for all \(z\) with \(\Im z {\gt} 1/2\).

Note that we can take the constants \(C_0\), \(C_{-2}\), and \(C_{-4}\) as

\begin{align} C_0 & = 9 \cdot 240^2 \cdot e^{\pi } \cdot \frac{E_4'(i/2)^{2}}{\Delta (i/2)} \notag \\ C_{-2} & = 3 \cdot \frac{E_4(i/2) E_4'(i/2)}{\Delta (i/2)} \notag \\ C_{-4} & = e^{-\pi } \cdot \frac{E_4(i/2)^{2}}{\Delta (i/2)}. \notag \end{align}
Lemma 7.8

For all \(n \in \mathbb {N}\), there exists a constant \(C'\) such that for all \(r \geq 0\),

\begin{align} r^n \cdot \int _{1}^{\infty } e^{-2\pi s} \, e^{-\pi r /s} \, \mathrm{d}s \leq C’ \end{align}
Proof

Fix \(n \in \mathbb {N}\). We know there exists a constant \(C\) such that for all \(x \geq 0\), \(\left\lvert x \right\rvert ^n \cdot \left\lvert e^{-\pi x} \right\rvert \leq C\). In particular, for all \(r \geq 0\) and \(s \geq 1\), \(r^n \cdot e^{-\pi r/s} \leq C s^n\). Hence, for all \(r \in \mathbb {R}\), we can write

\begin{align} r^n \cdot \int _{1}^{\infty } e^{-2\pi s} \, e^{-\pi r /s} \, \mathrm{d}{s} = \int _{1}^{\infty } e^{-2\pi s} \, \left(\left\lvert r \right\rvert ^n \cdot e^{-\pi r /s}\right) \, \mathrm{d}{s} \leq C \int _{1}^{\infty } e^{-2\pi s} \, s^n \, \mathrm{d}{s} \end{align}

The \(\Gamma \) function is given by

\begin{align} \Gamma (x) = \int _{0}^{\infty } e^{-u} \, u^{x-1} \, \mathrm{d}{u} \end{align}

for all \(x {\gt} 0\). Hence, writing \(u = 2\pi s\) and using \(\Gamma (n+1) = n!\), we get

\begin{align} C \int _{1}^{\infty } e^{-2\pi s} \, s^n \, \mathrm{d}{s} \leq C \int _{0}^{\infty } e^{-2\pi s} \, s^n \, \mathrm{d}{s} = C \int _{0}^{\infty } \frac{1}{(2\pi )^{n+1}} e^{-u} \, u^n \, \mathrm{d}{u} = \frac{C}{(2\pi )^n} \Gamma (n+1) = \frac{C \cdot n!}{(2\pi )^n} \end{align}

Defining \(C' := \frac{C \cdot n!}{(2\pi )^n}\) finishes the proof.

Lemma 7.9

There exists \(C {\gt} 0\) such that for all \(r \geq 0\),

\begin{equation} |I_1(r)|, |I_3(r)|, |I_5(r)| \leq C \int _1^{\infty } e^{-2\pi s} \, e^{-\pi r / s} \, \mathrm{d}s. \end{equation}
147

Proof

We only prove the bound for \(I_1(r)\), as the other two are similar. By 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} \, \mathrm{d}t. \]

With the change of variable \(s = 1 / t\), we get

\[ I_1(r) = i \int _1^{\infty } \phi _0(i s) \cdot s^{-4} \cdot e^{-\pi i r} \cdot e^{-\pi r / s} \, \mathrm{d}s \]

and the absolute value can be bounded as

\[ |I_1(r)| \leq \int _1^{\infty } |\phi _0(i s)| \cdot s^{-4} \cdot |e^{-\pi i r}| \cdot e^{-\pi r / s} \, \mathrm{d}s \le \int _1^{\infty } |\phi _0(is)| \cdot e^{-\pi r / s} \, \mathrm{d}s. \]

Now, Corollary 7.5 shows

\[ |I_1(r)| \leq C_0 \int _1^{\infty } e^{-2\pi s} \, e^{-\pi r / s} \, \mathrm{d}s. \]

Combined with Lemma 7.8, this shows that the integrals \(I_1\), \(I_3\), and \(I_5\) decay faster than any polynomial as \(r \to \infty \). For the integrals \(I_2\), \(I_4\), and \(I_6\), it is easier to see this since the contours are not touching the real axis.

Lemma 7.10

There exist \(C_1, C_2 {\gt} 0\) such that for all \(r \geq 0\),

\begin{equation} |I_2(r)|, |I_4(r)| \leq C_1 e^{-\pi r} \end{equation}
148

and

\begin{equation} |I_6(r)| \leq C_2 \frac{e^{-\pi (r + 2)}}{r + 2} \end{equation}
149

Proof

For \(I_2(r)\), parametrize \(z\) as \(z = t + i\) for \(t \in [-1,0]\), and we have

\[ 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} \, \mathrm{d}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 {\gt} 0\) such that \(|\phi _0\left(\frac{-1}{z+1}\right) (z + 1)^2| \leq C\), and the absolute value of the integral can be bounded by

\[ |I_2(r)| \le \int _{-1}^{0} C e^{-\pi r} \, \mathrm{d}t = C e^{-\pi r}. \]

The bound for \(I_4(r)\) is similar. For \(I_6(r)\), parametrize \(z\) as \(z = i t\) for \(t \in [1, \infty )\), and we have

\[ I_6(r) = 2 i \int _1^{\infty } \phi _0(i t) e^{-\pi r t} \, \mathrm{d}t \]

and the absolute value can be bounded as (using Corollary 7.5)

\[ |I_6(r)| \leq 2 \int _1^{\infty } |\phi _0(i t)| e^{-\pi r t} \, \mathrm{d}t \leq \frac{2C_0}{\pi } \int _1^{\infty } e^{-2\pi t} e^{-\pi r t} \, \mathrm{d}t = \frac{2C_0}{\pi } \frac{e^{-\pi (r + 2)}}{r + 2}. \]

Combining these, one can show that \(a\) is a Schwartz function.

Proposition 7.11

\(a(x)\) is a Schwartz function.

Proof

By Theorem 4.8, it suffices to show that the function is smooth and decays faster than any polynomial. The smoothness follows from the “differentiation under the integral”, which is already formalized in mathlib. The decay follows from Lemmas 7.9 and 7.10, together with Lemma 7.8.

\(a(x)\) satisfies 113.

Proof

We recall that the Fourier transform of a Gaussian function is

\begin{equation} \label{eqn:gaussian Fourier} \mathcal{F}(e^{\pi i \| x\| ^2 z})(y)=z^{-4}\, e^{\pi i \| y\| ^2 \, (\frac{-1}{z}) }. \end{equation}
150

Next, we exchange the contour integration with respect to \(z\) variable and Fourier transform with respect to \(x\) variable in ??. This can be done, since the corresponding double integral converges absolutely. In this way we obtain

\begin{align} \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\notag \\ -& 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.\notag \end{align}

Now we make a change of variables \(w=\frac{-1}{z}\). We obtain

\begin{align} \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\notag \\ +& \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.\notag \end{align}

Since \(\phi _0\) is \(1\)-periodic we have

\begin{align} \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\notag \\ +& 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\notag \\ \, =\, & a(y). \end{align}

This finishes the proof of the proposition.

Next, we check that \(a\) has double zeroes at all \(\Lambda _8\)-lattice points of length greater then \(\sqrt{2}\). Using 140, 141, and 142, we can control the behavior of \(\phi _0\) near \(0\) and \(i\infty \).

We have

\begin{align} \phi _0\left(\frac{i}{t}\right) & = O(e^{-2 \pi / t}) \quad \text{as } t \to 0 \label{eqn:phi0-near-0} \\ \phi _0\left(\frac{i}{t}\right) & = O(t^{-2}e^{2 \pi t}) \quad \text{as } t \to \infty . \label{eqn:phi0-near-infty} \\ \end{align}
Proof

The first estimate follows from 140 with \(z = i/t\). For the second estimate, by 119, 141, and 142, we have

\begin{equation} \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}). \end{equation}
156

For \(r{\gt}\sqrt{2}\) we can express \(a(r)\) in the following form

\begin{equation} \label{eqn: a double zeroes} a(r)=-4\sin (\pi r^2/2)^2\, \int \limits _{0}^{i\infty }\phi _0\Big(\frac{-1}{z}\Big)\, z^2\, e^{\pi i r^2 \, z}\, dz. \end{equation}
157

Proof

We denote the right hand side of 157 by \(d(r)\). Convergence of the integral for \(r {\gt} \sqrt{2}\) follows from Corollary 7.13. We can write

\begin{align} 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\notag \\ +& \int \limits _{1}^{i\infty +1}\phi _0\Big(\frac{-1}{z-1}\Big)\, (z-1)^2\, e^{\pi i r^2 \, z}\, dz.\notag \end{align}

From 119 we deduce that if \(r{\gt}\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

\begin{align} 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\notag \\ -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\notag \\ +& \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.\notag \end{align}

Now from 119 we find

\begin{align} & \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=\notag \\ & \phi _0(z+1)\, (z+1)^2-2\phi _0(z)\, z^2+\phi _0(z-1)\, (z-1)^2\notag \\ & -\frac{12i}{\pi }\, \Big(\phi _{-2}(z+1)\, (z+1)-2\phi _{-2}(z)\, z+\phi _{-2}(z-1)\, (z-1)\Big)\notag \\ & -\frac{36}{\pi ^2}\Big(\phi _{-4}(z+1)-2\phi _{-4}(z)+\phi _{-4}(z-1)\Big)=\notag \\ & 2\phi _0(z). \end{align}

Thus, we obtain

\begin{align} 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\notag \\ +& \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).\notag \end{align}

This finishes the proof.

Finally, we find another convenient integral representation for \(a\) and compute values of \(a(r)\) at \(r=0\) and \(r=\sqrt{2}\).

For \(r\geq 0\) we have

\begin{align} \label{eqn:a-another-integral}a(r)=& 4i\, \sin (\pi r^2/2)^2\, \Bigg(\frac{36}{\pi ^3\, (r^2-2)}-\frac{8640}{\pi ^3\, r^4}+\frac{18144}{\pi ^3\, r^2}\\ +& \int \limits _0^\infty \, \left(t^2\, \phi _0\Big(\frac{i}{t}\Big)-\frac{36}{\pi ^2}\, e^{2\pi t}+\frac{8640}{\pi }\, t-\frac{18144}{\pi ^2}\right)\, e^{-\pi r^2 t}\, dt \Bigg) .\notag \end{align}

The integral converges absolutely for all \(r\in \mathbb {R}_{\geq 0}\).

Proof

Suppose that \(r{\gt}\sqrt{2}\). Then by Proposition 7.14

\[ 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 119 we obtain

\begin{equation} \label{eqn: phi asymptotic} \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})\quad \mbox{as}\; t\to \infty . \end{equation}
160

For \(r{\gt}\sqrt{2}\) we have

\begin{equation} \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}.\end{equation}
161

Therefore, the identity 159 holds for \(r{\gt}\sqrt{2}\).

On the other hand, from the definition ?? we see that \(a(r)\) is analytic in some neighborhood of \([0,\infty )\). The asymptotic expansion 160 implies that the right hand side of 159 is also analytic in some neighborhood of \([0,\infty )\). Hence, the identity 159 holds on the whole interval \([0,\infty )\). This finishes the proof of the proposition.

From the identity 159 we see that the values \(a(r)\) are in \(i\mathbb {R}\) for all \(r\in \mathbb {R}_{\geq 0}\).

Proposition 7.16

We have \(a(0) = -\frac{i}{8640}\).

Proof

These identities follow immediately from the previous proposition.

Now we construct function \(b\). To this end we consider the function

Definition 7.17

\begin{equation} \label{eqn: h define} h(z) := 128 \frac{H_3(z) + H_4(z)}{H_2(z)^2}. \end{equation}
162

It is easy to see that \(h\in M^!_{-2}(\Gamma _0(2))\). Indeed, first we check that \(h|_{-2}\gamma =h\) for all \(\gamma \in \Gamma _0(2)\). Since the group \(\Gamma _0(2)\) is generated by elements \(\left(\begin{smallmatrix} 1 & 0 \\ 2 & 1 \end{smallmatrix}\right)\) and \(\left(\begin{smallmatrix} 1 & 1 \\ 0 & 1 \end{smallmatrix}\right)\) it suffices to check that \(h\) is invariant under their action. This follows immediately from 2729 and 162. Next we analyze the poles of \(h\). It is known [ 7 , Chapter I Lemma 4.1 ] that \(\theta _{10}\) has no zeros in the upper-half plane and hence \(h\) has poles only at the cusps. At the cusp \(i\infty \) this modular form has the Fourier expansion

\begin{equation} h(z)\, =\, q^{-1} + 16 - 132 q + 640 q^2 - 2550 q^3+O(q^4).\notag \end{equation}
163

Let \(I=\left(\begin{smallmatrix} 1 & 0 \\ 0 & 1 \end{smallmatrix}\right)\), \(T=\left(\begin{smallmatrix} 1 & 1 \\ 0 & 1 \end{smallmatrix}\right)\), and \(S=\left(\begin{smallmatrix} 0 & -1 \\ 1 & 0 \end{smallmatrix}\right)\) be elements of \(\Gamma _1\).

Definition 7.18

We define the following three functions

\begin{align} \psi _I\, :=\, & h-h|_{-2}ST \label{eqn:psiI-define}\\ \psi _T\, :=\, & \psi _I|_{-2}T \label{eqn:psiT-define}\\ \psi _S\, :=\, & \psi _I|_{-2}S. \label{eqn:psiS-define} \end{align}
Lemma 7.19

\(\psi _I(z), \psi _S(z), \psi _T(z)\) can be written as

\begin{align} \psi _I(z) & = \frac{H_4^3 (5 H_2^2 + 5 H_2 H_4 + 2 H_4^2)}{2\Delta }, \label{eqn:psiI-new} \\ \psi _S(z) & = -\frac{H_2^3 (2 H_2^2 + 5 H_2 H_4 + 5 H_4^2)}{2 \Delta }. \label{eqn:psiS-new} \\ \psi _T(z) & = \frac{H_3^3 (5 H_2^2 - 5 H_2 H_3 + 2 H_3^2)}{2 \Delta }\label{eqn:psiT-new} \end{align}
Proof

By Lemma 6.34, we have

\begin{align} 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. \end{align}

Using these equations and Lemma 6.42, we can rewrite \(\psi _I(z)\) as

\begin{align} \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} \\ & = 128 \frac{H_4^3(5 H_2^2 + 5 H_2 H_4 + 2 H_4^2)}{ H_2^2 H_3^2 H_4^3} \\ & = \frac{H_4^3 (5 H_2^2 + 5 H_2 H_4 + 2 H_4^2)}{2\Delta }. \end{align}

Applying \(|_{-2}S\) and \(|_{-2}T\) to the expression of \(\psi _I\) proves 167 and 168.

Now, we are ready to define function \(b\). Again, the definition here is slightly different from that in [ 11 ] , where all the contours are chosen to be the straight lines.

Definition 7.20

Define \(b_\mathrm{rad}: \mathbb {R}\to \mathbb {C}\) by

\begin{equation} b_\mathrm{rad}(r) := J_1(r) + J_2(r) + J_3(r) + J_4(r) + J_5(r) + J_6(r) \end{equation}
179

where for \(r \in \mathbb {R}\),

\begin{align} J_1(r) & := \int _{-1}^{-1 + i} \psi _T(z) e^{\pi i r z} \, \mathrm{d}z, \label{eqn:J1} \\ J_2(r) & := \int _{-1 + i}^{i} \psi _T(z) e^{\pi i r z} \, \mathrm{d}z, \label{eqn:J2} \\ J_3(r) & := \int _{1}^{1 + i} \psi _T(z) e^{\pi i r z} \, \mathrm{d}z, \label{eqn:J3} \\ J_4(r) & := \int _{1 + i}^{i} \psi _T(z) e^{\pi i r z} \, \mathrm{d}z, \label{eqn:J4} \\ J_5(r) & := -2 \int _{0}^{i} \psi _I(z) e^{\pi i r z} \, \mathrm{d}z, \label{eqn:J5} \\ J_6(r) & := -2 \int _{i}^{i \infty } \psi _S(z) e^{\pi i r z} \, \mathrm{d}z. \label{eqn:J6} \end{align}

Here all the contours are straight line segments. Then we define \(b : \mathbb {R}^8 \to \mathbb {C}\) by \(b(x) := b_\mathrm{rad}(\| x\| ^2)\).

Now we prove that \(b\) is a Schwartz function and satisfies condition 114. As in the case of \(a(x)\), we start with the following exponential bound of \(\psi _S(z)\) and \(\psi _I(z)\).

Lemma 7.21

There exist constants \(C_I, C_S, C_T {\gt} 0\) such that

\begin{align} |\psi _I(z)| & \le C_I e^{2\pi \Im z}, \label{eqn:psiI-bound} \\ |\psi _T(z)| & \le C_T e^{2\pi \Im z}, \label{eqn:psiT-bound} \\ |\psi _S(z)| & \le C_S e^{- \pi \Im z} \label{eqn:psiS-bound} \end{align}
Proof

The proof is similar to that of Lemma 7.5, follows from Lemma 7.4 and the fact that the vanishing orders of the numerators of \(\psi _I\), \(\psi _T\), and \(\psi _S\) at infinity are \(0\), \(0\) (i.e. not cusp forms), and \(\frac{3}{2}\) respectively.

Lemma 7.22
#

There exist a constant \(C {\gt} 0\) such that

\begin{align} |J_1(r)|, |J_3(r)|, |J_5(r)| & \le C \int _1^{\infty } e^{-\pi s} e^{\pi r / s}\, \mathrm{d}s. \end{align}
Lemma 7.23
#

There exist \(C_1, C_2 {\gt} 0\) such that

\begin{align} |J_2(r)|, |J_4(r)| & \le C_1 e^{-\pi r} \\ |J_6(r)| & \le C_2 \frac{e^{\pi (r + 1)}}{r + 1} \end{align}

Combining Lemmas 7.22, 7.23, and Theorem 4.8, we can prove that \(b(x)\) is a Schwartz function.

Proposition 7.24
#

\(b(x)\) is a Schwartz function.

\(b(x)\) satisfies 114.

Proof

Here, we repeat the arguments used in the proof of Proposition 7.12. We use identity 150 and change contour integration in \(z\) and Fourier transform in \(x\). Thus we obtain

\begin{align} \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 \notag \\ -& 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. \notag \end{align}

We make the change of variables \(w=\frac{-1}{z}\) and arrive at

\begin{align} \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 \notag \\ -& 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.\notag \end{align}

Now we observe that the definitions 163165 imply

\begin{align} \psi _T|_{-2}S=& -\psi _T \notag \\ \psi _I|_{-2}S=& \psi _S \notag \\ \psi _S|_{-2}S=& \psi _I. \notag \end{align}

Therefore, we arrive at

\begin{align} \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 \notag \\ +& 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 w}\, dw.\notag \end{align}

Now from ?? we see that

\[ \mathcal{F}(b)(x)=-b(x). \]

Now we regard the radial function \(b\) as a function on \(\mathbb {R}_{\geq 0}\). We check that \(b\) has double roots at \(\Lambda _8\)-points.

Corollary 7.26

We have

\begin{align} \psi _I(it) & = O(t^2 e^{\pi /t}) \quad \text{as } t \to 0 \label{eqn:psiI-near-0} \\ \psi _I(it) & = O(e^{2 \pi t}) \quad \text{as } t \to \infty . \label{eqn:psiI-near-infty} \end{align}
Proof

By 165, we have

\begin{equation} \psi _I(it) = (it)^{-2} \psi _S\left(\frac{-1}{it}\right) = -t^{-2} \psi _S\left(\frac{i}{t}\right). \end{equation}
194

and combined with 188 we get 192. 193 follows from Lemma 7.21.

For \(r{\gt}\sqrt{2}\) function \(b(r)\) can be expressed as

\begin{equation} \label{eqn: b double zeroes} b(r)=-4\sin (\pi r^2/2)^2\, \int \limits _{0}^{i\infty }\psi _I(z)\, e^{\pi i r^2 \, z}\, dz. \end{equation}
195

Proof

We denote the right hand side of 195 by \(c(r)\). By Corollary 7.26, the integral in 195 converges for \(r{\gt}\sqrt{2}\). Then we rewrite it in the following way:

\[ 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 ?? we know that \(\psi _I(z)=e^{-2\pi i z}+O(1)\) as \(\Im (z)\to \infty \). By assumption \(r^2{\gt}2\), hence we can deform the path of integration and write

\begin{align} \label{eqn: inside proof 1} \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. \end{align}

We have

\begin{align} \label{eqn: c1}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.\nonumber \end{align}

Next, we check that the functions \(\psi _I,\psi _T\), and \(\psi _S\) satisfy the following identity:

\begin{equation} \label{eqn: c2}\psi _T+\psi _S=\psi _I.\end{equation}
199

Indeed, from definitions 163-165 we get

\begin{align} \psi _T+\psi _S=& (h-h|_{-2}ST)|_{-2}T+(h-h|_{-2}ST)|_{-2}S\notag \\ =& h|_{-2}T-h|_{-2}ST^2+h|_{-2}S-h|_{-2}STS.\notag \end{align}

Note that \(ST^2S\) belongs to \(\Gamma _0(2)\). Thus, since \(h\in M^!_{-2}\Gamma _0(2)\) we get

\[ \psi _T+\psi _S=h|_{-2}T-h|_{-2}STS. \]

Now we observe that \(T\) and \(STS(ST)^{-1}\) are also in \(\Gamma _0(2)\). Therefore,

\[ \psi _T+\psi _S=h|_{-2}T-h|_{-2}STS=h|_{-2}-h|ST=\psi _I. \]

Combining 198 and 199 we find

\begin{align} 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\notag \\ & -2\int \limits _{i}^{i\infty }\psi _S(z)\, e^{\pi i r^2 \, z}\, dz\notag \\ =& b(r).\notag \end{align}

At the end of this section we find another integral representation of \(b(r)\) for \(r\in \mathbb {R}_{\geq 0}\) and compute special values of \(b\).

Proposition 7.28

For \(r\geq 0\) we have

\begin{equation} \label{eqn:b-another-integral}b(r)=4i\, \sin (\pi r^2/2)^2\, \left(\frac{144}{\pi \, r^2}+\frac{1}{\pi \, (r^2-2)}+\int \limits _0^\infty \, \left(\psi _I(it)-144-e^{2\pi t}\right)\, e^{-\pi r^2 t}\, dt\right).\end{equation}
200

The integral converges absolutely for all \(r\in \mathbb {R}_{\geq 0}\).

Proof

The proof is analogous to the proof of Proposition 7.15. First, suppose that \(r{\gt}\sqrt{2}\). Then by Proposition 7.27

\[ b(r)=4i\, \sin (\pi r^2/2)^2\, \int \limits _{0}^{\infty }\psi _I(it)\, e^{-\pi r^2 t}\, dt. \]

From ?? we obtain

\begin{equation} \label{eqn: psi asymptotic} \psi _I(it)=e^{2\pi t}+144+O(e^{-\pi t})\quad \mbox{as}\; t\to \infty . \end{equation}
201

For \(r{\gt}\sqrt{2}\) we have

\begin{equation} \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}.\end{equation}
202

Therefore, the identity 200 holds for \(r{\gt}\sqrt{2}\).

On the other hand, from the definition ?? we see that \(b(r)\) is analytic in some neighborhood of \([0,\infty )\). The asymptotic expansion 201 implies that the right hand side of 200 is also analytic in some neighborhood of \([0,\infty )\). Hence, the identity 200 holds on the whole interval \([0,\infty )\). This finishes the proof of the proposition.

We see from 200 that \(b(r)\in i\mathbb {R}\) far all \(r\in \mathbb {R}_\geq {0}\). Another immediate corollary of this proposition is

Proposition 7.29

We have \(b(0) = 0\).

Proof

These identities follow immediately from the previous proposition.