Tao Corollary 4.9: S_{eta^2,q}(x,0) = x(1+O*(0.02)) and major-arc L^2 mass >= 0.94x

With $S_{\eta,q}(x,\alpha)=\sum_{n}\Lambda(n)e(\alpha n)\mathbf 1_{(n,q)=1}\eta(n/x)$ as in Section 4, let $\eta$ be smooth, non-negative and supported in $[c,1]$ for some $0<c\le1$, normalised so that $\|\eta\|_{L^{2}(\mathbb R)}=1$; let $\tfrac1{2x}\le r<\tfrac12$, and let $q$ be a modulus all of whose prime factors are at most $\sqrt x$. Assume the five side conditions

1. $cx\ge10^{8}$;
2. $x\ge10^{4}\,\|\eta\eta'\|_{L^{1}(\mathbb R)}$;
3. $\log(cx)\ge5\,\|\eta\eta'\|_{L^{1}(\mathbb R)}$;
4. $x\ge10^{8}\,\|\eta\|_{L^{\infty}(\mathbb R)}^{4}$;
5. $rx\ge10\,\|\eta''\|_{L^{1}(\mathbb R)}\,\|\eta\|_{L^{\infty}(\mathbb R)}$.

Then

and

where $\mathcal O^{*}(E)$ denotes a quantity of absolute value at most $E$.

The second conclusion is the clean lower bound on the major-arc $L^{2}$ mass that Section 8 runs on: applied to the trapezoidal cutoff of that section it says that the major arc carries at least $0.94\|\eta\|_{L^{2}}^{2}x$ of the mass of the sifted prime exponential sum.

Quoted inputs The proof in the source invokes three explicit estimates of Rosser and Schoenfeld, none of which is available in the ambient library, and each appears here as a hypothesis in exactly the form used: $\psi(y)=y+\mathcal O^{*}\bigl(y/(40\log cx)\bigr)$ for $cx\le y\le x$; $\psi(x)\le1.04\,x$; and $\omega(q)\log x\le2.52\sqrt x$, which is what $\pi(\sqrt x)\le1.26\sqrt x/\log\sqrt x$ gives for $q$ the product of the primes up to $\sqrt x$. Here $\psi(y)=\sum_{n\le y}\Lambda(n)$ and $\omega(q)$ is the number of distinct prime factors of $q$.

Fidelity note Condition 5 is the source's $rx\ge20\|\eta'\eta'+\eta\eta''\|_{L^{1}}\|\eta\|_{L^{\infty}}$ rewritten with $\tfrac12\|\eta''\|_{L^{1}}$ in place of $\|\eta'\eta'+\eta\eta''\|_{L^{1}}$, matching the constant that the proof of Proposition 4.8 actually yields. The numerology of the corollary is unchanged.

Formalization Note Frequencies are real numbers, so for $r\le\tfrac12$ the region $\|\alpha\|_{\mathbb R/\mathbb Z}\le r$ is the interval $[-r,r]$. The first conclusion is stated as a bound on $\bigl|S_{\eta^{2},q}(x,0)-x\bigr|$ by $0.02\,x$.