Tao five primes: sums, kernels and Fourier transforms for the sub-decomposition

Definition

TaoFivePrimes_Explicit

by tabbott · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-number-theorycircle-methodfive-primesgoldbachnumber-theory

Auxiliary definitions for the sub-decomposition of the three frontier estimates in Tao's five-primes theorem (Propositions 8.3, 8.4 and equation (8.18) of the paper), on top of Def_TaoFivePrimes_ArcSplit.

$e_\mathbb{R}(t) = e^{2\pi i t}$ (eR), and the Fourier transform $\hat\eta(\xi) = \int_\mathbb{R} \eta(y)\, e(\xi y)\,dy$ (hat) of a real cutoff — the paper's normalisation, eq. (2.6).
Sun η y α $= \sum_{n \le y} \Lambda(n)\,\eta(n/y)\, e(\alpha n)$ , the unsifted exponential sum over the real line (the object controlled by the explicit formula, Proposition 7.2).
Ssift η y α $= \sum_{n \le y} \Lambda^\sharp(n)\,\eta(n/y)\, e(\alpha n)$ on the circle $\mathbb{R}/\mathbb{Z}$ , with $\Lambda^\sharp$ the $\sqrt{\cdot}$ -primorial-sifted von Mangoldt function of the paper (Section 8) — S1 x and S0 x from Def_TaoFivePrimes_ArcSplit are Ssift eta1 x and Ssift eta0 (x/1000) definitionally.
kernelH H α $= \sum_{1 \le n \le H} e(\alpha n)$ on the circle, and its real-line counterpart DR H α $= \sum_{1 \le n \le H/3} e(\alpha n)$ ; DK H = kernelH (H/3) by rfl.
arcRadius x $= T_0/(3.6\pi x)$ , the major-arc radius of eq. (8.12) with $T_0 = 3.29\times 10^9$ .
mainIntegrand x α $= \hat\eta_1(\alpha x)^2\,\hat\eta_0(\alpha x/1000)\, e(-x\alpha)$ , the integrand of the main term of Proposition 8.3.
zetaZeroCount T, the number of zeros of $\zeta$ in the critical strip with $0 \le \operatorname{Im}\rho \le T$ .

Definition code

import Definitions.Def_TaoFivePrimes_ArcSplit
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.NumberTheory.LSeries.RiemannZeta

/-!
# Real-variable objects for the proof of Tao's Theorem 8.2

Source: Terence Tao, https://arxiv.org/abs/1201.6656. The smoothed unsifted prime sum
`S_{η,1}(y, α)` of (4.1) (with `q = 1`), the general sifted sum `S_{η,√y♯}(y, α)`, Tao's
Fourier transform `η̂(ξ) = ∫ η(y) e(ξy) dy` (Section 7), the real-variable Dirichlet kernel,
the radius of the strongly major arc, and the count `N(T)` of zeros of `ζ` in the strip up to
height `T` (Theorem 1.5, Proposition 7.2).
-/

open scoped BigOperators
open MeasureTheory

namespace TaoFivePrimes

/-- `e(t) = exp(2πit)` on the real line. -/
noncomputable def eR (t : ℝ) : ℂ := Complex.exp (2 * Real.pi * Complex.I * t)

/-- Tao's Fourier transform `η̂(ξ) := ∫_ℝ η(y) e(ξy) dy` (Section 7, before (7.3)). -/
noncomputable def hat (η : ℝ → ℝ) (ξ : ℝ) : ℂ := ∫ y : ℝ, (η y : ℂ) * eR (ξ * y)

/-- The unsifted smoothed prime sum `S_{η,1}(y, α) = ∑_{n ≤ y} Λ(n) η(n/y) e(αn)` of (4.1)
with `q = 1`, for a cutoff `η` supported in `[0, 1]`. -/
noncomputable def Sun (η : ℝ → ℝ) (y : ℝ) (α : ℝ) : ℂ :=
  ∑ n ∈ Finset.range (⌊y⌋₊ + 1),
    ((ArithmeticFunction.vonMangoldt n : ℝ) * η ((n : ℝ) / y) : ℝ) * eR (α * n)

/-- The general sifted sum `S_{η,√y♯}(y, α)` as a function on the circle, sieving at
`√⌊y⌋` as in `siftedVonMangoldt`. `S1 x = Ssift eta1 x` and `S0 x = Ssift eta0 (x/1000)`
up to the evaluation of `η` (see the structural theorems `S1_eq_Ssift`, `S0_eq_Ssift`). -/
noncomputable def Ssift (η : ℝ → ℝ) (y : ℝ) (α : AddCircle (1 : ℝ)) : ℂ :=
  TaoFourierIdentity.fourierPolynomial (Finset.range (⌊y⌋₊ + 1))
    (fun n ↦ (siftedVonMangoldt ⌊y⌋₊ n * η ((n : ℝ) / y) : ℝ)) (fun n ↦ (n : ℤ)) α

/-- The Dirichlet-type kernel `D_H(α) = ∑_{1 ≤ h ≤ H} e(hα)` of Proposition 4.10, on the circle.
`DK H = kernelH (H / 3)` definitionally. -/
noncomputable def kernelH (H : ℕ) (α : AddCircle (1 : ℝ)) : ℂ :=
  TaoFourierIdentity.fourierPolynomial (Finset.Icc 1 H) (fun _ ↦ 1) (fun n ↦ (n : ℤ)) α

/-- The kernel `D_{H/3}` as a function of a real frequency. -/
noncomputable def DR (H : ℕ) (α : ℝ) : ℂ := ∑ n ∈ Finset.Icc 1 (H / 3), eR (α * n)

/-- The radius `T₀ / (3.6 π x)` of the strongly major arc (Proposition 8.3). -/
noncomputable def arcRadius (x : ℕ) : ℝ := T0 / (3.6 * Real.pi * x)

/-- The main-term integrand of (8.14): `η̂₁(αx)² η̂₀(αx/K) e(-xα)` at `K = 1000`. -/
noncomputable def mainIntegrand (x : ℕ) (α : ℝ) : ℂ :=
  hat eta1 (α * x) ^ 2 * hat eta0 (α * x / 1000) * eR (-(x : ℝ) * α)

/-- `N(T)`: the number of zeros of `ζ` in the strip `{0 < Re s < 1, 0 ≤ Im s ≤ T}`
(Theorem 1.5, Proposition 7.2). -/
noncomputable def zetaZeroCount (T : ℝ) : ℕ :=
  {s : ℂ | riemannZeta s = 0 ∧ 0 < s.re ∧ s.re < 1 ∧ 0 ≤ s.im ∧ s.im ≤ T}.ncard

theorem DK_eq_kernelH (H : ℕ) (α : AddCircle (1 : ℝ)) : DK H α = kernelH (H / 3) α := rfl

end TaoFivePrimes

Source

T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014), 997-1038, https://arxiv.org/abs/1201.6656, Sections 2, 7 and 8 (eqs. (2.6), (8.10)-(8.12))

View graph