Explicit BV eta0 major-arc error before numerical specialization

Open

TaoFivePrimes.eta0_prop72_bv_explicit_error

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

exponential-sumsnumber-theorytao-five-primes

Put $T_0=3.29\times10^9$ and let $\eta_0$ be Tao's logarithmic triangular cutoff, supported on $[1/4,1]$ . For every real $y\ge4000$ and $|\theta|\le T_0/(4\pi y)$ , the modulus-one von Mangoldt sum satisfies

\left|S_{\eta_0,1}(y,\theta)-y\int_{\mathbb R}\eta_0(t)e(\theta yt)\,dt\right|\le \frac{(252+256\log2)\log T_0}{3T_0}y+4.02\times10^{10}\sqrt y.

This is the explicit analytic input before the large-scale numerical specialization in Section 8. The constants retain $\|\eta_0\|_1=1$ , $\|\eta_0'\|_1=8\log2$ , and total variation $\|D^2\eta_0\|=48$ , together with the verified-height zero count $N(T_0)\le10^{10}$ . The theorem includes the verification-height input and the limiting argument extending the smooth Proposition 7.2 to this literal nonsmooth cutoff. In particular, the smooth proposition alone is not a proof. The coefficient $252+256\log2$ is retained exactly; the printed subsequent comparison with $330$ is not used.

Preamble

import Definitions.Def_TaoFivePrimes_ArcSplit
import Definitions.Def_TaoFivePrimes_SmoothedExpSum

Formal statement

theorem TaoFivePrimes.eta0_prop72_bv_explicit_error
    (y : ℝ) (hy : 4000 ≤ y) (theta : ℝ)
    (hup : |theta| ≤ TaoFivePrimes.T0 / (4 * Real.pi * y)) :
    ‖TaoFivePrimes.smoothedExpSum TaoFivePrimes.eta0 1 y theta -
        (y : ℂ) * ∫ t : ℝ, (TaoFivePrimes.eta0 t : ℂ) *
          TaoFivePrimes.expCircle (theta * y * t)‖ ≤
      ((252 + 256 * Real.log 2) * Real.log TaoFivePrimes.T0 /
        (3 * TaoFivePrimes.T0)) * y +
      ((402 : ℝ) / 100 * 10 ^ 10) * Real.sqrt y := by sorry

Source

T. Tao, Every odd number greater than 1 is the sum of at most five primes, arXiv:1201.6656v4, Proposition 7.2, equations (7.3)-(7.4), printed p.34; cutoff norms (5.9), (5.11), (5.13), printed p.26, and preceding mollification convention; Section8 eta0 specialization, printed p.38. https://arxiv.org/pdf/1201.6656

View graph