Piecewise-smooth eta0 explicit-formula error with derivative masses

Open

TaoFivePrimes.eta0_prop72_piecewise_error

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

exponential-sumsnumber-theorytao-five-primes

Write $T_0=3.29\times10^9$ and let $\eta_0$ be the logarithmic triangular cutoff. For real $y\ge4000$ and $|\theta|\le T_0/(4\pi y)$ , the modulus-one prime sum obeys

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

where the coefficient retains the classical derivative masses:

A=60\int\eta_0+32\int|\eta_0'|+4\left(36+\int|\eta_0''|\right).

The constant $36$ accounts for the derivative jumps of absolute sizes $16,16,4$ at $1/4,1/2,1$ . The theorem includes the distributional integration-by-parts or mollification justification, the verified-height zeta-zero input and zero-count estimate. It must not be inferred directly from the smooth statement by treating classical second derivatives as the complete distributional derivative. The separate derivative-mass theorems evaluate the three integrals to $1$ , $8\log2$ and $12$ .

Preamble

import Definitions.Def_TaoFivePrimes_ArcSplit
import Definitions.Def_TaoFivePrimes_SmoothedExpSum

Formal statement

theorem TaoFivePrimes.eta0_prop72_piecewise_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)‖ ≤
      ((60 * (∫ t : ℝ, TaoFivePrimes.eta0 t) +
          32 * (∫ t : ℝ, |deriv TaoFivePrimes.eta0 t|) +
          4 * (36 + ∫ t : ℝ, |deriv (deriv TaoFivePrimes.eta0) t|)) *
        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