Tao Corollary 3.9: subdivision form of the odd-restricted bilinear large sieve

Proved

TaoFivePrimes.large_sieve_subdivision

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

analytic-number-theoryexponential-sumsgoldbachlarge-sievenumber-theory

Let $I,J\subset\mathbb R$ be intervals of length at least $2$ , let $\alpha\in\mathbb R$ , let $M\ge1$ , and let $(a_n)_{n\in\mathbb Z}$ and $(b_m)_{m\in\mathbb Z}$ be square-summable complex sequences. Then

\left|\ \sum_{n\in I\cap\mathbb Z}\ \sum_{m\in J\cap\mathbb Z}a_n\mathbf 1_{(n,2)=1}\,b_m\mathbf 1_{(m,2)=1}\,e(nm\alpha)\right| \;\le\;\left(\tfrac12|I|+\frac{1}{\displaystyle\inf_{1\le j\le M}\|4j\alpha\|_{\mathbb R/\mathbb Z}}\right)^{1/2} \left(\left\lfloor\frac{|J|}{2M}\right\rfloor+1\right)^{1/2}\|a\|_{\ell^2(\mathbb Z)}\,\|b\|_{\ell^2(\mathbb Z)},

where $e(t)=e^{2\pi i t}$ , $|I|$ and $|J|$ are the lengths of the two intervals, and $\|t\|_{\mathbb R/\mathbb Z}$ is the distance from $t$ to the nearest integer.

Corollary 3.8 is the case $M=|J|/2$ , in which $J$ is not subdivided at all. That form is useful only when the multiples $4j\alpha$ stay away from the origin for every $j$ up to $|J|/2$ , which fails once $J$ is long; the present corollary trades a factor $\bigl(\lfloor|J|/(2M)\rfloor+1\bigr)^{1/2}$ for the freedom to impose the separation condition only up to a chosen height $M$ . It is the form of the large sieve applied to the Type II bilinear sums of Section 5, where $M$ is chosen so that $\|4j\alpha\|$ is controlled by the rational approximation to $\alpha$ .

Quoted input Corollary 3.7, the bilinear special case of the large sieve inequality that the source deduces from the large sieve inequality of Montgomery's survey, is not available in the ambient library and appears here as a hypothesis, in the generality the deduction requires.

Formalization Note Intervals are given by their real endpoints and are taken half-open, so that the integers they contain are described by integer floor bounds. Square-summability of the two sequences is assumed explicitly: the source's convention makes the right-hand side infinite, and the statement vacuous, when it fails, whereas the ambient convention would evaluate the divergent sum as $0$ . The infimum over $1\le j\le M$ is carried as an explicit positive lower bound, which is how the corollary is applied and which avoids a nonemptiness side condition.

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_Explicit

open Finset

Formal statement

theorem TaoFivePrimes.large_sieve_subdivision (a b : ℤ → ℂ)
    (ha : Summable (fun n : ℤ => ‖a n‖ ^ 2)) (hb : Summable (fun n : ℤ => ‖b n‖ ^ 2))
    (alpha : ℝ) (xI yI xJ yJ M : ℝ)
    (hI : 2 ≤ yI - xI) (hJ : 2 ≤ yJ - xJ) (hM : 1 ≤ M)
    (delta : ℝ) (hdelta : 0 < delta)
    (hd : ∀ j : ℤ, 1 ≤ j → (j : ℝ) ≤ M →
      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)) :
    ‖∑ n ∈ (Finset.Ioc ⌊xI⌋ ⌊yI⌋).filter (fun n : ℤ => Odd n),
        ∑ m ∈ (Finset.Ioc ⌊xJ⌋ ⌊yJ⌋).filter (fun m : ℤ => Odd m),
          a n * b m * TaoFivePrimes.eR (alpha * (n : ℝ) * (m : ℝ))‖
      ≤ Real.sqrt ((yI - xI) / 2 + 1 / delta)
          * Real.sqrt ((⌊(yJ - xJ) / (2 * M)⌋₊ : ℝ) + 1)
          * Real.sqrt (∑' n : ℤ, ‖a n‖ ^ 2) * Real.sqrt (∑' n : ℤ, ‖b n‖ ^ 2) := 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 3, Corollary 3.9 (Subdivision)

View graph