5 Poisson summation

For \(s=(s_0,s_1,s_2)\) invariant under Galois, let \(H(P,s)\) be the toric height and \(Z(s)\) the sum of \(H(P,s)^{-1}\) over integral rational torus points. The function \(1^{D_0}\) imposes integrality at the finite places. Fourier transforms use the Haar measures of the paper, and \(e(t)=\exp (2\pi it)\). The computation starts with the local factors and then applies Poisson summation. Later, \(Z_0(z)=Z(2z,0,0)=\sum _{n\geq 1}d_n n^{-z}\) and \(R(z)\) denotes the correction Euler product. In the spectral formulas write \(s=(s_0,\sigma ,\sigma )\), \(t=m(v_0)\), and \(\lambda =\sigma -\pi it\).

Theorem 6 The multivariate height zeta function

✓

Fix any \(s \in (\mathbb {C}^{\Sigma (1)})^{\Gamma }\) with \(\mathrm{Re}(s_0+s_1+s_2) {\gt} 2\). Then the multivariate Dirichlet series

\begin{equation*} Z(s)= \sum _{\substack {P \in T(\mathbb Q)\\ { \text{\emph{integral}} }}} H(P,s)^{-1} \end{equation*}

is absolutely convergent and equals

\begin{align*} \left({1-3^{-z}}\right) \zeta (z) \prod _{q\equiv 2\pmod{3}} \left(1+\frac{1}{q^{z}}\right)^{-1} \prod _{p\equiv 1\pmod{3}} \left(1+\frac{3}{p^z}\left(1-\frac{1}{p^z}\right)^{-1}\right) \end{align*}

where \(z = \frac{1}{2}(s_0+s_1+s_2)\). This multivariate Dirichlet series admits a meromorphic continuation to \(\{ s \in (\mathbb {C}^{\Sigma (1)})^{\Gamma } : \mathrm{Re}(s_0+s_1+s_2) {\gt} 1\} \).

Proof in Lean ▼

Compute the local Fourier transforms, apply Poisson summation, and evaluate the resulting real integral by residues. Shift the height parameters to obtain the full convergence region, then identify the continued Euler product.

The proof assumes Poisson summation (Equation 15).

Proposition 4 The local integral condition

✓

Let \(v\) be a finite place of \(\mathbb {Q}\) and let \(w\) be a place of \(E\) lying over \(v\).

If \(v \neq 3\), then \(1_v^{D_0}(x) = 1\) if and only if \(\ell _w(x) \in \mathbb R_{\geq 0}v_1+\mathbb R_{\geq 0}v_2\). In particular \(K_v^{D_0}=K_v^{\mathrm{max}}\).
Let \(v = 3\), let \(w\) be the unique place of \(E\) over \(3\), and let \(\mathfrak w = (1-\zeta )O_{E,w}\) be the maximal ideal of \(O_{E,w}\), so that \(3O_{E,w} = \mathfrak w^2\). The support of \(1_3^{D_0}\) is the subgroup

\begin{equation*} K_{3,2}\mathrel {:=}\iota ^{-1}(1+\mathfrak w^2) =\iota ^{-1}(1+3O_{E,w})\subset K_3^{\mathrm{max}}. \end{equation*}
Let \(K^{\mathrm{max}}=\prod _v K_v^{\mathrm{max}}\) and \(K^{D_0}=\prod _v K_v^{D_0}\subset K^{\mathrm{max}}\). The latter is the subgroup which fixes the characteristic function \(1^{D_0}=\otimes _v1_v^{D_0}\) for integral points in \(T(\mathbb {A})\), with \(1_\infty ^{D_0}=1\). Then

\[ K_3^{D_0}=K_{3,2},\qquad K^{D_0}=K_{3,2}\times \prod _{v\neq 3}K_v^{\mathrm{max}}. \]

Proof in Lean ▼

Away from \(3\), evaluate the invariant functions in local coordinates to obtain the cone condition. At \(3\), the same computation gives the subgroup \(1+3O_{E,w}\). Its stabilizer determines the global compact level.

Equation 15

✓

Let \(f\in L^1(T(\mathbb {A}))\) and suppose \(\widehat f|_{T(\mathbb {Q})^\perp }\in L^1(T(\mathbb {Q})^\perp )\). With counting measure on \(T(\mathbb {Q})\) and the normalized dual measure, the following equality holds for almost every \(y\in T(\mathbb {A})\).

\begin{equation*} \int _{T(\mathbb {Q})} f(xy)\, dx = \int _{T(\mathbb {Q})^\perp } \widehat{f}(\chi ) \chi (y) \, d\chi \end{equation*}

This is an explicit hypothesis in the formalization.

Proposition 5 Local Fourier transforms

✓

Let \(s \in (\mathbb {C}^{\Sigma (1)})^{\Gamma }\) and assume \(\mathrm{Re}(s_e){\gt}0\) for each \(e \in \{ 0,1,2\} \). Let \(w\) be the infinite place of \(E\). Let \(\chi \in T(\mathbb {R})^\vee \) be a unitary character. If \(\chi \) is ramified then \(\widehat{H_\infty }(\chi ,-s,D_0)\) is identically zero. If \(\chi \) is unramified, then \(\chi (x)= e(\langle \ell _w(x) ,m\rangle )\) for all \(x \in T(\mathbb {R})\) for a unique \(m \in \mathfrak t^\vee \), and

\begin{equation*} \widehat{H_\infty }(\chi ,-s,D_0) = \left(\frac{-1}{2\pi i}\right) \frac{s_0+s_1+s_2}{2\pi i} \frac{1}{(m(v_0)+\frac{s_0}{2\pi i})(m(v_0)-\frac{s_1+s_2}{2\pi i})}. \end{equation*}

Next let \(v\) be a finite place of \(\mathbb {Q}\). For any unitary character \(\chi \in T(\mathbb {Q}_v)^\vee \), the integral defining \(\widehat{H_v}(\chi ,-s,D_0)\) converges absolutely to a holomorphic function of \(s\) in the region

\[ \{ s \in (\mathbb {C}^{\Sigma (1)})^\Gamma : \mathrm{Re}(s_1),\mathrm{Re}(s_2){\gt}0 \} . \]

Assume \(v \neq 3\). Let \(w\) be any place of \(E\) lying over \(v\). The local characteristic function \(1_v^{D_0}\) is \(K_v^{\mathrm{max}}\)-invariant. If \(\chi \) is ramified, then \(\widehat{H_v}(\chi ,-s,D_0)\) is identically zero. If \(\chi \) is unramified then we may regard \(\chi \) as a character on \(X_\ast (T_{E})^{\Gamma (w/v)}\) (Proposition 1) and

\begin{equation*} \widehat{H_v}(\chi ,-s,D_0) = \sum _{\substack {n \in X_\ast (T_{E})^{\Gamma (w/v)}\\ { n \in \mathbb R_{\geq 0}v_1+\mathbb R_{\geq 0}v_2 }} } \chi (n)^{-1} q_v^{\varphi (n)} . \end{equation*}

If \(v = 3\) then the support of \(x \mapsto H_3(x,-s,D_0)\) is the congruence subgroup \(K_{3,2}\) of \(K_3^{\mathrm{max}}\) of index six. Under the isomorphism \(\iota :T(\mathbb {Q}_3)\to E_w^\times \) the support corresponds to the subgroup \(1+3O_{E,w}\) of \(O_{E,w}^\times \) where \(w\) is the unique place of \(E\) lying over \(3\).

Proof in Lean ▼

At infinity and at finite places other than \(3\), ramified characters vanish after integration over the maximal compact subgroup. For unramified characters, integrate the archimedean support function on its two cones and sum the finite valuation lattices. At \(3\), integrate over the congruence subgroup of index six.

Equation 16

✓

\begin{equation*} \widehat{H_\infty }(\chi ,-s,D_0) = \left(\frac{-1}{2\pi i}\right) \frac{s_0+s_1+s_2}{2\pi i} \frac{1}{(m(v_0)+\frac{s_0}{2\pi i})(m(v_0)-\frac{s_1+s_2}{2\pi i})}. \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 17

✓

Proof in Lean ▼

The linked Lean proof establishes this statement.

Remark 2 Why the parameters are kept separate

✓

The local Fourier transforms — and therefore the entire Poisson summation argument — must be computed before restricting to the line in \(\mathrm{Pic}^T(S) \otimes \mathbb {C}\) spanned by the \(T_E\)-line bundle \(\mathcal O(D_0)\) of interest since \(x \mapsto H_v(x,-s,D_0)\) will not be integrable for any place \(v \neq 3,\infty \) once either of \(s_1\) or \(s_2\) vanishes, no matter how large and positive \(\mathrm{Re}(s_0)\) is.

Proof in Lean ▼

Along a boundary ray where a height exponent vanishes, the local valuation series has terms of constant absolute value. It therefore fails to converge.

Equation 18

✓

\begin{equation*} \int _{T(\mathbb {Q}_v)} H_v(x,s)^{-1}1_v^{D_0}(x)\chi (x)^{-1}\, d^\times x_v =\sum _{n \in N_w} q_v^{\frac{1}{e_v}\varphi (n)} 1_v^{D_0}(n) \chi (n)^{-1} = \sum _{\substack {n \in X_\ast (T_{E})^{\Gamma (w/v)}\\ { n \in \mathbb R_{\geq 0}v_1+\mathbb R_{\geq 0}v_2 }} } \chi (n)^{-1} q_v^{\varphi (n)} . \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 19

✓

\begin{equation*} \ell (x)(\mathrm{N}) = -\log |\mathrm{N}(x)|_{\mathbb {A}} \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Proposition 6 The adelic logarithm

✓

There is an exact sequence

\begin{equation*} 1 \longrightarrow K^{\mathrm{max}}/\mu ^{\mathrm{max}} \longrightarrow T(\mathbb Q)\backslash T(\mathbb {A}) \xrightarrow {\ell } \mathfrak t \longrightarrow 0 \end{equation*}

where \(K^{\mathrm{max}}\) is the maximal compact subgroup of \(T(\mathbb {A})\) and \(\mu ^{\mathrm{max}} = T(\mathbb {Q}) \cap K^{\mathrm{max}}\).

Proof in Lean ▼

The product formula makes the logarithm descend to the adelic quotient. Principalize the finite valuations to identify its kernel with the compact quotient; the infinite component supplies surjectivity.

Lemma 4 The quotient by the integral level

✓

Let \(K^{D_0}=K_{3,2}\times \prod _{v\neq 3}K_v^{\mathrm{max}}\) be the subgroup of \(K^{\mathrm{max}}\) fixing \(1^{D_0}\), as in Proposition 4. The map \(\ell \) induces an isomorphism

\begin{equation*} T(\mathbb {Q})\backslash T(\mathbb {A})/K^{D_0} \xrightarrow {\sim } \mathfrak t. \end{equation*}

Let \(a(u)\in T(\mathbb {A})\) have infinite component \(\iota ^{-1}(e^u)\) and all finite components one, so \(\ell (a(u))=uv_0\). In this coordinate, the pushforward of the quotient measure is \(du/6\).

Proof in Lean ▼

The six Eisenstein units represent the residue classes at the ramified place. They identify the quotient by the integral level with the logarithm line. Tracking the normalized Haar measure gives \(du/6\).

Equation 20

✓

\begin{equation*} \chi _m(x)=e(\langle m,\ell (x)\rangle ), \qquad m\in \mathfrak t^\vee . \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Lemma 5 The finite Fourier product

✓

For \(\operatorname {Re}(\sigma ){\gt}1\) and \(t\in \mathbb {R}\), put \(\lambda =\sigma -\pi it\). Then

\begin{equation*} \widehat{H_{\mathrm{fin}}}(\chi _m,-s,D_0) =\frac16 \prod _{q\equiv 2\pmod3}(1-q^{-2\lambda })^{-1} \prod _{p\equiv 1\pmod3} \frac{1+2p^{-\lambda }}{(1-p^{-\lambda })^2} \end{equation*}

and

\begin{equation*} \left|\widehat{H_{\mathrm{fin}}}(\chi _m,-s,D_0)\right| \leq \widehat{H_{\mathrm{fin}}}(\chi _0,{-\operatorname {Re}(s)},D_0){\lt}\infty . \end{equation*}

Here \(\chi _0\) is the trivial character, corresponding to \(m=0\). The Euler product converges absolutely and locally uniformly for \(\operatorname {Re}(\lambda ){\gt}1\) and is bounded on every half-plane \(\operatorname {Re}(\lambda )\geq \tau {\gt}1\).

Proof in Lean ▼

Sum the local valuation series separately at split and inert primes and include the factor \(1/6\) at \(3\). A convergent positive Euler product bounds the absolute values and proves locally uniform convergence.

Equation 21

✓

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 22

✓

\begin{equation*} \left|\widehat{H_{\mathrm{fin}}}(\chi _m,-s,D_0)\right| \leq \widehat{H_{\mathrm{fin}}}(\chi _0,{-\operatorname {Re}(s)},D_0){\lt}\infty . \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Lemma 6 Convergence before Poisson summation

✓

Let \(s=(s_0,\sigma ,\sigma )\in (\mathbb {C}^{\Sigma (1)})^\Gamma \) with \(\operatorname {Re}(s_0){\gt}0\) and \(\operatorname {Re}(\sigma ){\gt}1\), and put \(f=H(\cdot ,-s,D_0)\). Then \(f\in L^1(T(\mathbb {A}))\) and \(\widehat f\, |_{T(\mathbb {Q})^\perp }\in L^1(T(\mathbb {Q})^\perp )\).

Proof in Lean ▼

The positive local factors give spatial integrability. The finite Euler-product bound and quadratic decay of the archimedean factor give integrability on the annihilator of \(T(\mathbb {Q})\).

Equation 23

✓

\begin{equation*} \begin{aligned} \widehat{H_\infty }(\chi _{m,\infty },-s,D_0) & =\frac1{s_0+2\pi it}+\frac1{2\sigma -2\pi it}\\ & =\frac{s_0+2\sigma }{(s_0+2\pi it)(2\sigma -2\pi it)}. \end{aligned}\end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Lemma 7 Applying Poisson summation

✓

For \(s\) as in Lemma 6, we have

\begin{equation*} Z(s)=6\int _\mathbb {R}\widehat{H_\infty }(\chi _{m,\infty },-s,D_0) \widehat{H_{\mathrm{fin}}}(\chi _m,-s,D_0)\, dt, \end{equation*}

where both the series defining \(Z(s)\) and the integral converge absolutely.

Proof in Lean ▼

Apply the general Poisson formula with the normalized quotient measure. Identify the characters trivial on the integral level with the real logarithm coordinate; the dual measure contributes the factor six.

The proof assumes Poisson summation (Equation 15).

Equation 24

✓

\begin{equation*} Z(s)=6\int _\mathbb {R}\widehat{H_\infty }(\chi _{m,\infty },-s,D_0) \widehat{H_{\mathrm{fin}}}(\chi _m,-s,D_0)\, dt, \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

The proof assumes Poisson summation (Equation 15).

Equation 25

✓

\begin{equation*} \operatorname {div}(\chi ^{a'+b'}) =\sum _{i=0}^2\langle a’+b’,v_i\rangle D_i =-2D_0+D_1+D_2. \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 26

✓

\begin{equation*} R(z)=\prod _{q\equiv 2\pmod3}\left(1-q^{-2z}\right) \prod _{p\equiv 1\pmod3}\left(1-3p^{-2z}+2p^{-3z}\right). \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Lemma 8 Dedekind zeta factorization

✓

The height zeta function is also given by

\begin{align*} Z(s)=\left(1-3^{-z}\right)^2\xi (z)^2R(z),\qquad z=\tfrac 12(s_0+s_1+s_2), \end{align*}

where \(\xi \) is the Dedekind zeta function of the cyclotomic field \(\mathbb {Q}(\sqrt{-3})\). The height zeta function has meromorphic continuation to the region \(\{ s \in (\mathbb {C}^{\Sigma (1)})^{\Gamma } : \mathrm{Re}(s_0+s_1+s_2) {\gt} 1\} \).

Proof in Lean ▼

Compare the Euler factors with \(\xi (z)^2\) and the correction product \(R(z)\). The factorization and convergence of the correction product give the continuation.

The proof assumes Poisson summation (Equation 15).

Equation 27

✓

\begin{equation*} Z_0(z)=\left(1-3^{-z}\right)^2\xi (z)^2R(z). \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

The proof assumes Poisson summation (Equation 15).

Remark 3 The coefficients

✓

Comparing Euler factors in 27 gives the coefficients explicitly: \(d_n=0\) if \(3\mid n\), and if \(3\nmid n\) then

\[ d_n=\sum _{d\mid n}3^{\omega (d_1)}(-1)^{\Omega (d_2)}, \]

where \(d=d_1d_2\) with \(d_1\) divisible only by primes \(p\equiv 1\pmod3\) and \(d_2\) only by primes \(q\equiv 2\pmod3\). Equivalently, \(d_n\) is the product of \(3k+1\) over prime powers \(p^k\parallel n\) with \(p\equiv 1\pmod3\) if every prime \(q\equiv 2\pmod3\) divides \(n\) to an even power, and \(d_n=0\) otherwise.

Proof in Lean ▼

Expand the split, inert, and ramified Euler factors and multiply the prime-power coefficients.

The proof assumes Poisson summation (Equation 15).

Proposition 7 Laurent coefficients

✓

The only pole of \(Z_0(z)\) in the half-plane \(\mathrm{Re}(z){\gt}1/2\) is a double pole at \(z=1\). Its Laurent expansion there is

\begin{equation*} Z_0(z)=\frac{\alpha }{9(z-1)^2} +\frac{2\alpha }{9}\left(\mu -\frac{\zeta '(2)}{\zeta (2)}+\beta +\frac38\log 3\right)\frac{1}{z-1}+O(1), \end{equation*}

where \(\alpha \) and \(\beta \) are as in 1.

Proof in Lean ▼

Expand the Dedekind zeta factor at \(1\) and logarithmically differentiate the convergent correction product. Simplifying the prime factors yields \(\alpha \), \(\beta \), and the Euler–Kronecker constant \(\mu \).

The proof assumes Poisson summation (Equation 15).

Equation 28

✓

\begin{equation*} Z_0(z)=\frac{\alpha }{9(z-1)^2} +\frac{2\alpha }{9}\left(\mu -\frac{\zeta '(2)}{\zeta (2)}+\beta +\frac38\log 3\right)\frac{1}{z-1}+O(1), \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 29

✓

Here \(r=\operatorname {Res}_{z=1}\xi (z)=\pi /(3\sqrt3)\) and \(\mu \) is the Euler–Kronecker constant defined above.

\begin{equation*} Z_0(z)=\frac{a}{(z-1)^2} +2a\left(\mu +\frac12\log 3+\frac{R'(1)}{2R(1)}\right)\frac{1}{z-1} +O(1), \qquad a=\frac49r^2R(1). \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.