Second-order Fourier decay of eta0 from variation forty-eight

Proved

TaoFivePrimes.eta0_fourier_decay_second_variation

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

bounded-variationfourier-analysistao-five-primes

For every nonzero real frequency $\beta$ , the logarithmic triangular cutoff satisfies the second-order Fourier decay estimate

\left|\int_{\mathbb R}\eta_0(t)e(\beta t)\,dt\right|\le\frac{48}{(2\pi\beta)^2}.

The constant includes the total variation of the distributional second derivative: the classical density contributes $12$ , and the derivative jumps contribute $16+16+4=36$ . This gives the second-order integration-by-parts input for the explicit-formula major-arc estimates without incorrectly treating the nonsmooth cutoff as twice continuously differentiable. The existing first-order Fourier bound has numerator $8\log2$ and one power of frequency; this theorem supplies quadratic decay.

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_RepresentationCount
import Definitions.Def_TaoFivePrimes_SmoothedExpSum

open MeasureTheory

Formal statement

theorem TaoFivePrimes.eta0_fourier_decay_second_variation (beta : ℝ) (hbeta : beta ≠ 0) :
    ‖∫ t : ℝ, (TaoFivePrimes.eta0 t : ℂ) * TaoFivePrimes.expCircle (beta * t)‖ ≤
      48 / (2 * Real.pi * beta) ^ 2 := by sorry

Source

T. Tao, Every odd number greater than 1 is the sum of at most five primes, arXiv:1201.6656v4, Fourier integration-by-parts principle Lemma3.1 and cutoff norms (5.11)-(5.13), with the distributional interpretation described on printed p.26; used in the Proposition7.2 analytic mechanism. https://arxiv.org/pdf/1201.6656

View graph