Theorem 1.3 — explicit estimate for the smoothed exponential sum

Theorem 1.3 (Exponential sum estimate). Let $x \geq 10^{20}$ be a real number, and suppose that

for an integer $a$ and a natural number $q$ with $100 \leq q \leq x/100$, $(a,q) = 1$, and $|\beta| \leq 1/q^2$. Let $q_0$ be a natural number all of whose prime factors are at most $\sqrt{x}$. Then

This is the main exponential sum estimate of Tao's five-primes paper, and its durable content: the constants are small enough to be useful for $x$ between roughly $10^{30}$ and $10^{1300}$, a range in which the asymptotically superior estimates of Vinogradov, Chen–Daboussi and Ramaré carry constants that are either too large or not effective. It is the standard input to explicit Goldbach-type results, and it has since been improved by Helfgott and Platt but not superseded in method.

On the hypotheses. All four are load-bearing. The lower bound $x \geq 10^{20}$ is needed for the stated constants; the mission's range begins at $8.7 \times 10^{36}$, so it is satisfied there, but the estimate is false for small $x$ without it. The condition on $q_0$ is the one most easily lost, since Section 1 describes the modulus as being of minor technical importance and advises ignoring it at a first reading; it is what admits the choice $q_0 = \prod_{p \leq \sqrt{x}} p$ used at level $x$ in Section 8, and hence what connects this estimate to the sums appearing in the Fourier expression (8.11) for the weighted representation count.

Note that it is $4\alpha$, not $\alpha$, that is approximated by the rational $a/q$. As Section 1 explains, this is a consequence of allowing the modulus $q_0 = 2$, which restricts the sum to odd $n$ and saves a factor of two in the explicit constants.

Scope. This is (1.9) only. The refinements (1.10) for $q \leq x^{1/3}$, (1.11) for $q \geq x^{2/3}$, and (1.12) for $q \geq x^{2/3}$ with $a = \pm 1$ are separate statements and are not asserted here; they are needed for $q$ near $1$ and near $x$, where (1.9) alone is not sufficient for the argument of Section 8.

Formalization notes. $S_{\eta_0,q_0}$ is smoothedExpSum eta0 q₀ x α, using the published cutoff eta0. The hypothesis $\beta \in [-1/q^2, 1/q^2]$ is written as $|\beta| \leq 1/q^2$. The numerator $a$ ranges over $\mathbb{Z}$ and the coprimality condition is imposed on its absolute value. The real power $x^{4/5}$ is Real.rpow.