Tao Section 6 from the corrected minor arc bound

Proved

TaoFivePrimes.exp_sum_estimate_from_corrected_minor_arc_bound

by Hartmann_Psi · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theoryexponential-sumsgoldbachnumber-theory

Let $x\ge10^{20}$ , let $4\alpha=\frac aq+\beta$ with $100\le q\le x/100$ , $(a,q)=1$ and $|\beta|\le q^{-2}$ , and let every prime factor of the sifting modulus $q_0$ be at most $\sqrt x$ . Assume the minor-arc bound in the form the source's own argument supports: for every admissible pair $U,V$ — that is, $1<U,V<x$ with $UV\le\frac x4$ , $UV^2\ge x$ and $U,V\ge40$ —

\begin{aligned} |S_{\eta_0,2}(x,\alpha)|\ \le\ & 0.5\,\frac xq(\log x)\Bigl(\log\Bigl(\frac{2UV}{q}+4\Bigr)+4\Bigr)+0.89\Bigl(UV+\frac52q\Bigr)(8+\log q)\log(2x)\\ &+\Bigl(0.1\frac{x}{\sqrt q}+0.39\frac{x}{\sqrt{x/q}}\Bigr)\Bigl(\log\frac{x}{UV}\Bigr)\log\frac{Vx}{U}+\Bigl(0.55\frac{x}{\sqrt U}+1.1\frac{x}{\sqrt V}\Bigr)\log\frac xU . \end{aligned}

Then

|S_{\eta_0,q_0}(x,\alpha)|\ \le\ \Bigl(0.14\frac{x}{\sqrt q}+0.64\frac{x}{\sqrt{x/q}}+0.15\,x^{4/5}\Bigr)(\log x)(\log x+11.3).

This is the source's Section 6 run from the weakened minor-arc bound rather than from the printed one, and it shows that the two corrections to the printed constants — the additive $4$ in the first term and $1.1$ in place of $0.78$ in the last — cost nothing downstream: the exponential sum estimate of Theorem 1.3 comes out unchanged. The content is the choice

U=\tfrac14x^{2/5},\qquad V=\tfrac12x^{2/5},

for which the admissibility conditions hold once $x\ge10^{20}$ , followed by the numerical collapse of the four resulting terms and the passage from the sifting modulus $2$ to the general modulus $q_0$ through the source's Lemma 4.1, which is public and proved on the platform as TaoFivePrimes.smoothedExpSum_modulus_change.

Formalization Note The minor-arc bound is carried as a hypothesis quantified over all admissible $U,V$ , so that this statement isolates exactly the content of Section 6 and can be proved independently of Section 5. The power $x^{4/5}$ is the real power x ^ (4/5 : ℝ).

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_SmoothedExpSum
import Definitions.Def_TaoFivePrimes_RepresentationCount

open Finset

Formal statement

theorem TaoFivePrimes.exp_sum_estimate_from_corrected_minor_arc_bound
    (x α β : ℝ) (a : ℤ) (q q₀ : ℕ)
    (hx : (10 : ℝ) ^ 20 ≤ x)
    (hq : 100 ≤ q) (hqx : (q : ℝ) ≤ x / 100)
    (haq : Nat.Coprime a.natAbs q)
    (hα : 4 * α = (a : ℝ) / q + β)
    (hβ : |β| ≤ 1 / (q : ℝ) ^ 2)
    (hq₀ : ∀ p ∈ q₀.primeFactors, (p : ℝ) ≤ Real.sqrt x)
    (hminor : ∀ U V : ℝ, 1 < U → 1 < V → U < x → V < x → U * V ≤ x / 4 → x ≤ U * V ^ 2 →
        40 ≤ U → 40 ≤ V →
        ‖TaoFivePrimes.smoothedExpSum TaoFivePrimes.eta0 2 x α‖ ≤
          0.5 * (x / q) * Real.log x * (Real.log (2 * U * V / q + 4) + 4)
            + 0.89 * (U * V + (5 / 2) * q) * (8 + Real.log q) * Real.log (2 * x)
          + (0.1 * x / Real.sqrt q + 0.39 * x / Real.sqrt (x / q))
              * Real.log (x / (U * V)) * Real.log (V * x / U)
          + (0.55 * x / Real.sqrt U + 1.1 * x / Real.sqrt V) * Real.log (x / U)) :
    ‖TaoFivePrimes.smoothedExpSum TaoFivePrimes.eta0 q₀ x α‖ ≤
      (0.14 * x / Real.sqrt q + 0.64 * x / Real.sqrt (x / q) + 0.15 * x ^ (4 / 5 : ℝ))
        * Real.log x * (Real.log x + 11.3) := by sorry

Source

Terence Tao, "Every odd number greater than 1 is the sum of at most five primes", Mathematics of Computation 83 (2014), 997-1038; arXiv:1201.6656, https://arxiv.org/abs/1201.6656, Section 6 (Proof of Theorem 1.3), run from the weakened form of Theorem 5.1

View graph