Full-circle mesoscopic L² bound for eta₁

Proved

TaoFivePrimes.minor_arc_L2_full_circle_8001

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

analytic-number-theoryfive-primeslarge-sievenumber-theory

Let $x$ be an integer satisfying

8.7\times 10^{36}\le x\le e^{3100},

and put $N_0=4\times10^{14}$ and $m=\lfloor N_0/3\rfloor$ . Let $S_1(x,\alpha)$ be Tao's sifted prime exponential sum with cutoff $\eta_1$ , and let

D_m(\alpha)=\sum_{1\le h\le m} e(h\alpha).

Then the full-circle weighted second moment satisfies

\int_{\mathbb R/\mathbb Z} |S_1(x,\alpha)|^2 |D_m(\alpha)|^2\,d\alpha \le 8.001\,m^2x.

This is the mesoscopic large-sieve input used before subtracting the mass on the strongly major arc.

Formalization Note The integer $m$ is natural-number division $N_0/3$ , followed by coercion to the real numbers. Haar measure on the period-one additive circle is probability-normalized.

Preamble

import Definitions.Def_TaoFivePrimes_ArcSplit

open MeasureTheory

Formal statement

namespace TaoFivePrimes

theorem minor_arc_L2_full_circle_8001 (x : ℕ)
    (h1 : 87 * 10 ^ 35 ≤ x)
    (h2 : (x : ℝ) ≤ Real.exp 3100) :
    (∫ α, ‖S1 x α‖ ^ 2 * ‖DK (4 * 10 ^ 14) α‖ ^ 2
      ∂AddCircle.haarAddCircle) ≤
      8.001 * ((4 * 10 ^ 14 / 3 : ℕ) : ℝ) ^ 2 * x := by
  sorry

end TaoFivePrimes

Source

Terence Tao, “Every odd number greater than 1 is the sum of at most five primes,” Mathematics of Computation 83 (2014), 997–1038, arXiv:1201.6656v4, https://arxiv.org/abs/1201.6656. Proposition 4.10 and equation (4.15), specialized in Section 8 in the proof of Proposition 8.4 at the displayed 8.001 bound immediately after the definition H := floor(N₀/3); equation (8.3) gives ||η₁||∞ = 1.

View graph