Tao Section 5: the pointwise bound for the dyadic Type II sums

Proved

TaoFivePrimes.typeII_pointwise

by Hartmann_Psi · Sep 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theoryexponential-sumsgoldbachlarge-sievenumber-theory

Let $x>0$ and $W,q\ge2$ , and suppose both intervals $[\frac W2,W]$ and $[\frac{x}{2W},\frac xW]$ have length at least $2$ . Let $\alpha$ be a frequency for which

\delta\ \le\ \|4j\alpha\|_{\mathbb R/\mathbb Z}\qquad(1\le j\le q/2),

i.e. $\delta$ is a lower bound for the separation $\inf_{1\le j\le q/2}\|4j\alpha\|$ . Let $(a_n)$ be supported on the odd integers of $(\frac W2,W]$ with $|a_n|\le\frac12\log n$ there, and $(b_m)$ supported on the odd integers of $(\frac{x}{2W},\frac xW]$ with $|b_m|\le1$ . Then

\Bigl|\sum_{n}\sum_{m}a_nb_m\,e(\alpha nm)\Bigr|\ \le\ \frac12\Bigl(\frac W4+\frac1\delta\Bigr)^{1/2}\Bigl(\Bigl\lfloor\frac{x}{2Wq}\Bigr\rfloor+1\Bigr)^{1/2}\Bigl(\bigl(\tfrac W4+1\bigr)\log^2W\Bigr)^{1/2}\Bigl(\frac{x}{4W}+1\Bigr)^{1/2}.

This is the pointwise estimate for the dyadic pieces $F(W)$ of the Type II sum in the source's minor-arc theorem, with the two $\ell^2$ masses already evaluated. In the application $a_n=g(n)$ is the centred divisor coefficient of Vaughan's identity, for which $|g(n)|\le\frac12\log n$ , and $b_m=\mu(m)$ , for which $|\mu(m)|\le1$ ; the two intervals are the dyadic ranges of $w$ and $d$ . The subdivision form of the odd-restricted bilinear large sieve is applied with subdivision parameter $M=q/2$ , and the resulting $\ell^2$ masses are the source's

A=\sum_{d\in[\frac x{2W},\frac xW]}\mathbf 1_{(d,2)=1}\le\frac x{4W}+1,\qquad B=\sum_{w\in[\frac W2,W]}\mathbf 1_{(w,2)=1}\log^2w\le\Bigl(\frac W4+1\Bigr)\log^2W;

the factor $\frac12$ in front is the one produced by $|g|\le\frac12\log$ .

Formalization Note The subdivision corollary and the two counting bounds are imported; the large sieve inequality itself, which the subdivision corollary quotes, is carried through as the hypothesis hsls. Intervals are half-open with integer floor endpoints. The separation $\delta$ is given as an explicit lower bound rather than as an infimum, which is how it is used and which avoids a nonemptiness side condition; in the application $\delta=\frac1{2q}$ by the source's computation (ala).

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_Explicit

open Finset

Formal statement

theorem TaoFivePrimes.typeII_pointwise (x W q alpha delta : ℝ)
    (hx : 0 < x) (hW : 2 ≤ W) (hq : 2 ≤ q) (hdelta : 0 < delta)
    (hIlen : 2 ≤ W / 2) (hJlen : 2 ≤ x / (2 * W))
    (hd : ∀ j : ℤ, 1 ≤ j → (j : ℝ) ≤ q / 2 →
      delta ≤ |(j : ℝ) * (4 * alpha) - round ((j : ℝ) * (4 * alpha))|)
    (hsls : ∀ (a' b' : ℤ → ℂ), Summable (fun n : ℤ => ‖a' n‖ ^ 2) →
        Summable (fun n : ℤ => ‖b' n‖ ^ 2) →
        ∀ beta u1 v1 u2 v2 d : ℝ, 1 ≤ v1 - u1 → 1 ≤ v2 - u2 → 0 < d →
        (∀ j : ℤ, 1 ≤ j → (j : ℝ) ≤ v2 - u2 →
          d ≤ |(j : ℝ) * beta - round ((j : ℝ) * beta)|) →
        ‖∑ n ∈ Finset.Ioc ⌊u1⌋ ⌊v1⌋, ∑ m ∈ Finset.Ioc ⌊u2⌋ ⌊v2⌋,
            a' n * b' m * TaoFivePrimes.eR (beta * (n : ℝ) * (m : ℝ))‖
          ≤ Real.sqrt ((v1 - u1) + 1 / d)
              * Real.sqrt (∑' n : ℤ, ‖a' n‖ ^ 2) * Real.sqrt (∑' n : ℤ, ‖b' n‖ ^ 2))
    (a b : ℤ → ℂ)
    (ha0 : ∀ n, n ∉ (Finset.Ioc ⌊W / 2⌋ ⌊W⌋).filter (fun n : ℤ => Odd n) → a n = 0)
    (hb0 : ∀ m, m ∉ (Finset.Ioc ⌊x / (2 * W)⌋ ⌊x / W⌋).filter (fun m : ℤ => Odd m) → b m = 0)
    (hab : ∀ n ∈ (Finset.Ioc ⌊W / 2⌋ ⌊W⌋).filter (fun n : ℤ => Odd n),
      ‖a n‖ ≤ (1 / 2) * Real.log (n : ℝ))
    (hbb : ∀ m ∈ (Finset.Ioc ⌊x / (2 * W)⌋ ⌊x / W⌋).filter (fun m : ℤ => Odd m), ‖b m‖ ≤ 1) :
    ‖∑ n ∈ (Finset.Ioc ⌊W / 2⌋ ⌊W⌋).filter (fun n : ℤ => Odd n),
        ∑ m ∈ (Finset.Ioc ⌊x / (2 * W)⌋ ⌊x / W⌋).filter (fun m : ℤ => Odd m),
          a n * b m * TaoFivePrimes.eR (alpha * (n : ℝ) * (m : ℝ))‖
      ≤ (1 / 2) * Real.sqrt (W / 4 + 1 / delta)
          * Real.sqrt ((⌊x / (2 * W * q)⌋₊ : ℝ) + 1)
          * Real.sqrt ((W / 4 + 1) * Real.log W ^ 2)
          * Real.sqrt (x / (4 * W) + 1) := by sorry

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.6656, https://arxiv.org/abs/1201.6656, Section 5 (Minor arcs), subsection "Estimation of the Type II sum", equation (del1) together with the bounds |A| <= x/(4W)+1 and |B| <= (W/4+1) log^2 W that follow it

View graph