Tao, Proposition 7.2 — major arc sums (positive scale, zeros with multiplicity)

Proposition 7.2 (Major arc sums). Let $T_0 = 3.29 \times 10^9$ be the height of Theorem 1.5. Let $\eta:\mathbb R\to\mathbb R$ be a smooth non-negative function supported on $[c,c']$ with $c>0$, and let $x,\alpha$ be reals with $cx \geq 10^3$ and

Then

where

and $N(T_0)$ is the number of zeroes of $\zeta$, counted with multiplicity, in the strip $\{0 \leq \Re(s) \leq 1,\ 0 \leq \Im(s) \leq T_0\}$. Here $S_{\eta,1}(x,\alpha)=\sum_{n}\Lambda(n)\,\eta(n/x)\,e(\alpha n)$ and $e(\theta)=e^{2\pi i\theta}$.

Role. This is the estimate that controls the exponential sum on the major arc $\alpha = O(T_0/x)$ by comparing it with the archimedean integral $x\int\eta(y)e(\alpha xy)\,dy$. The error is governed by the zeroes of $\zeta$ below height $T_0$, which is where the numerical verification of Theorem 1.5 enters. It feeds the strongly major arc estimate of Section 8.

Relation to TaoFivePrimes.major_arc_sums. That earlier node transcribed the proposition without the positivity of $c$, which the source takes for granted since $\eta$ lives on $\mathbb R^+$ and $[c,c']$ is a support interval. It was disproved by taking $c<0$, $x<0$, $c'=0$, where Lean's conventions $\sqrt{c}=0$ and $a/0=0$ make the right-hand side negative. This node restores exactly that hypothesis; $x>0$ then follows from $cx\ge10^3$. It also counts zeroes with multiplicity, as the source's proof requires: the explicit formula sums over zeroes with multiplicity, and each zero with $|\Im\rho|\le T_0$ contributes at most $c^{-1/2}x^{1/2}\|\eta\|_{L^1}$. The earlier node used the number of distinct zeroes, which is only equivalent given simplicity of the zeroes, an input the source does not use.

Formalization notes. $N(T_0)$ is the finite sum of analyticOrderNatAt riemannZeta s over the zeroes $s$ in the closed strip. The strip contains finitely many zeroes, and at each of them $\zeta$ is analytic (they avoid the pole $s=1$) and not locally zero, so this is the order of vanishing, i.e. the multiplicity. The constant $A$ is inlined; the $L^1$ norms are the integrals $\int|\eta|$, $\int|\eta'|$, $\int|\eta''|$ with iterated deriv. The height $T_0$ is the literal $3.29\times10^9$, so a proof is expected to import riemann_verified. Support on $[c,c']$ is expressed as $\eta(y)\ne0\to y\in[c,c']$, and $c^{-1/2}$, $x^{1/2}$ as 1 / Real.sqrt c, Real.sqrt x. No hypothesis $c\le c'$ is needed: if $c>c'$ then $\eta\equiv0$ and both sides vanish.