Fourier inversion and tail bridge for the major-arc cutoffs

Proved

TaoFivePrimes.strongly_major_arc_eta_cutoff_fourier_bridge_source

by marwahaha · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisgoldbachnumber-theory

For the literal cutoffs $\eta_1,\eta_0$ and the centered arc $A$ of radius $T_0/(3.6\pi x)$ , the scaled truncated Fourier integral

x\int_A E_1(\alpha)^2E_0(\alpha)e(-x\alpha)\,d\alpha

differs by at most $0.01$ from the full convolution

\int_{\mathbb R}\int_{\mathbb R}\eta_1(s)\eta_1(1-s-t/1000)\eta_0(t)\,ds\,dt.

The result isolates ordinary Fourier inversion and the explicit tail estimate; it contains no assertion about primes or zeta zeros.

Preamble

import Definitions.Def_TaoFivePrimes_ArcSplit
import Definitions.Def_TaoFivePrimes_stronglyMajorCutoffModel
import Mathlib.MeasureTheory.Integral.Bochner.Set

open MeasureTheory

Formal statement

namespace TaoFivePrimes

theorem strongly_major_arc_eta_cutoff_fourier_bridge_source (x : ℕ)
    (h1 : 87 * 10 ^ 35 ≤ x) :
    let A : Set (AddCircle (1 : ℝ)) :=
      Metric.closedBall 0 (3.29 * 10 ^ 9 / (3.6 * Real.pi * (x : ℝ)))
    let cutoffCoefficient : ℂ :=
      ∫ t : ℝ, ∫ s : ℝ,
        (((eta1 s * eta1 (1 - s - t / 1000) * eta0 t : ℝ) : ℂ))
    ‖(x : ℂ) *
          (∫ alpha in A,
            stronglyMajorCutoffModel eta1 (x : ℝ) alpha ^ 2 *
              stronglyMajorCutoffModel eta0 ((x : ℝ) / 1000) alpha *
              fourier (-(x : ℤ)) alpha
              ∂AddCircle.haarAddCircle) -
        cutoffCoefficient‖ ≤ (1 / 100 : ℝ) := by
  sorry

end TaoFivePrimes

Source

Terence Tao, Every odd number greater than 1 is the sum of at most five primes, arXiv:1201.6656v4, proof of Proposition 8.3, Fourier inversion and tail estimate after equation (8.15), https://arxiv.org/abs/1201.6656

View graph