Proposition 8.3: the strongly major arc estimate (8.12)

Open

TaoFivePrimes.major_arc_estimate

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

additive-number-theorycircle-methodfive-primesgoldbachnumber-theory

Strongly major arc estimate (Proposition 8.3). Let $8.7\times10^{36}\le x\le e^{3100}$ be an integer, $K=1000$ , $N_0=4\times10^{14}$ , $T_0=3.29\times10^9$ . Then

\int_{\|\alpha\|_{\mathbb R/\mathbb Z}\le\frac{T_0}{3.6\pi x}} S_{\eta_1,\sqrt x\sharp}(x,\alpha)^2\,S_{\eta_0,\sqrt{x/K}\sharp}(x/K,\alpha)\,D_{N_0/3}(\alpha)^3\,e(-x\alpha)\,d\alpha \;=\; \frac{x^2}{K}\Big(\frac{N_0}{3}\Big)^3\Big(\frac23+\mathcal O^*(0.1)\Big),

i.e. the integral over the strongly major arc differs from $\frac23\cdot\frac{x^2}{K}(N_0/3)^3$ by at most $0.1\cdot\frac{x^2}{K}(N_0/3)^3$ in absolute value. Here $N_0/3$ is the integer $\lfloor N_0/3\rfloor$ , matching the length of the kernel DK.

This is the main term of the circle-method argument for Theorem 8.2. In the paper it is proved from: the mean-value bound (8.13) $D_{N_0/3}(\alpha)=(N_0/3)(1+\mathcal O^*(10^{-10}))$ on the arc; Proposition 7.2 (the von Mangoldt explicit formula with the zeros of $\zeta$ up to height $T_0$ — this is where Theorem 1.5, the numerical verification of RH, enters), which gives $S_{\eta_0,1}(x/K,\alpha)=\frac xK(\hat\eta_0(\alpha x/K)+\mathcal O^*(10^{-6}))$ and $S_{\eta_1,1}(x,\alpha)=x(\hat\eta_1(\alpha x)+\mathcal O^*(10^{-6}))$ on the arc; Lemma 4.1 to remove the sieve; Corollary 4.7 and Lemma 4.3 to control the error terms (8.15)–(8.16) by $0.02x$ ; and the calculus identity $\int\eta_1(s)\eta_1(1-s-t/K)\,ds=1+\mathcal O^*(10/K)$ using (8.1), (8.4), (8.5).

The integral is over the probability Haar measure on $\mathbb R/\mathbb Z$ , restricted to majorArc x; the integrand is representationIntegrand, which equals the displayed product by representationIntegrand_eq.

Preamble

import Definitions.Def_TaoFivePrimes_ArcSplit
open MeasureTheory

Formal statement

namespace TaoFivePrimes

theorem major_arc_estimate (x : ℕ) (h1 : 87 * 10 ^ 35 ≤ x) (h2 : (x : ℝ) ≤ Real.exp 3100) :
    ‖(∫ α in majorArc x, representationIntegrand x (4 * 10 ^ 14) α ∂AddCircle.haarAddCircle)
        - ((2 / 3 * ((x : ℝ) ^ 2 / 1000 * ((4 * 10 ^ 14 / 3 : ℕ) : ℝ) ^ 3) : ℝ) : ℂ)‖
      ≤ 0.1 * ((x : ℝ) ^ 2 / 1000 * ((4 * 10 ^ 14 / 3 : ℕ) : ℝ) ^ 3) := by sorry

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, Section 8, Proposition 8.3, eq. (8.12), pp. 38-41

View graph