Tao Corollary 4.9: normalized raw major-arc mass estimate

Proved

TaoFivePrimes.S1_major_arc_L2_mass_corollary49_raw

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

additive-number-theoryanalytic-number-theoryfourier-analysisgoldbachnumber-theory

For an integer $x$ in Tao's large-number range, put

r=\frac{T_0}{3.6\pi x},\qquad T_0=3.29\times10^9.

Assume the two radius bounds $1/(2x)\le r\le 1/2$ and the five explicit hypotheses obtained from Corollary 4.9 after taking $c=1/10$ and normalizing the Section 8 trapezoid by $\eta=\sqrt{3/2}\,\eta_1$ . Then there is a real $\varepsilon$ with $|\varepsilon|\le0.02$ such that

0.999\,[0.99(1+\varepsilon)]^2x\le \frac32\int_{\operatorname{majorArc}(x)}|S_1(x,\alpha)|^2\,d\alpha.

The factor $3/2$ records the squared normalization because $\|\eta_1\|_2^2=2/3$ . Keeping $\varepsilon$ exposes the exact coefficient before the paper rounds the lower bound to $0.94$ .

Preamble

import Definitions.Def_TaoFivePrimes_ArcSplit

open MeasureTheory
open TaoFivePrimes

Formal statement

theorem TaoFivePrimes.S1_major_arc_L2_mass_corollary49_raw (x : ℕ)
    (hr_lower : 1 / (2 * (x : ℝ)) ≤ T0 / (3.6 * Real.pi * (x : ℝ)))
    (hr_upper : T0 / (3.6 * Real.pi * (x : ℝ)) ≤ 1 / 2)
    (hc8 : (10 ^ 8 : ℝ) ≤ (1 / 10 : ℝ) * x)
    (hneat : (10 ^ 4 : ℝ) * (3 / 2 : ℝ) ≤ x)
    (halamo : 5 * (3 / 2 : ℝ) ≤ Real.log ((1 / 10 : ℝ) * x))
    (h10q : (10 ^ 8 : ℝ) * (9 / 4 : ℝ) ≤ x)
    (hr0b : 20 * 60 * Real.sqrt (3 / 2 : ℝ) ≤ T0 / (3.6 * Real.pi)) :
    ∃ eps : ℝ, |eps| ≤ 0.02 ∧
      0.999 * (0.99 * (1 + eps)) ^ 2 * x ≤
        (3 / 2 : ℝ) *
          ∫ alpha in majorArc x, ‖S1 x alpha‖ ^ 2 ∂AddCircle.haarAddCircle := by
  sorry

Source

Terence Tao, Every odd number greater than 1 is the sum of at most five primes, arXiv:1201.6656v4, Corollary 4.9 (eqs. 4.8–4.14) specialized in Section 8 using eqs. 8.2, 8.3, 8.7, and 8.9, https://arxiv.org/html/1201.6656v4

View graph