Positive-scale smooth Proposition 7.2 on quarter-to-one support

Open

TaoFivePrimes.prop72_smooth_quarter_support

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

explicit-formulaexponential-sumstao-five-primes

Let $\eta$ be smooth, nonnegative and supported on $[1/4,1]$ . For $y\ge4000$ and $|\theta|\le T_0/(4\pi y)$ , where $T_0=3.29\times10^9$ , the prime-sum error satisfies

\left|S_{\eta,1}(y,\theta)-y\int\eta(t)e(\theta yt)\,dt\right|\le \frac{(60\|\eta\|_1+32\|\eta'\|_1+4\|\eta''\|_1)\log T_0}{3T_0}y+4.02\times10^{10}\sqrt y\,\|\eta\|_1.

This is Proposition 7.2 at fixed positive support parameters $c=1/4,c'=1$ , retaining the verified-height RH and zero-count input as part of the proof obligation. In particular, it does not use the disproved unrestricted platform statement: positivity of the support and scale is explicit here. The second derivative is classical because the cutoff is smooth. The theorem is intended to pass to the literal nonsmooth cutoff through a separate controlled inward approximation.

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_ArcSplit
import Definitions.Def_TaoFivePrimes_SmoothedExpSum

open MeasureTheory

Formal statement

theorem TaoFivePrimes.prop72_smooth_quarter_support
    (eta : ℝ → ℝ) (hsmooth : ContDiff ℝ (⊤ : ℕ∞) eta)
    (hnonneg : ∀ t, 0 ≤ eta t)
    (hsupp : ∀ t, eta t ≠ 0 → t ∈ Set.Icc (1 / 4 : ℝ) 1)
    (y : ℝ) (hy : 4000 ≤ y) (theta : ℝ)
    (hup : |theta| ≤ TaoFivePrimes.T0 / (4 * Real.pi * y)) :
    ‖TaoFivePrimes.smoothedExpSum eta 1 y theta -
        (y : ℂ) * ∫ t : ℝ, (eta t : ℂ) * TaoFivePrimes.expCircle (theta * y * t)‖ ≤
      (60 * (∫ t : ℝ, eta t) + 32 * (∫ t : ℝ, |deriv eta t|) +
        4 * (∫ t : ℝ, |deriv (deriv eta) t|)) *
        (Real.log TaoFivePrimes.T0 / (3 * TaoFivePrimes.T0)) * y +
      ((402 : ℝ) / 100 * 10 ^ 10) * Real.sqrt y * (∫ t : ℝ, eta t) := by sorry

Source

T. Tao, arXiv:1201.6656v4, Proposition7.2 equations(7.3)-(7.4), printed p.34, with c=1/4,c′=1, positive y≥4000, and N(T0)≤10^10 stated immediately after the proposition. https://arxiv.org/pdf/1201.6656

View graph