Tao Corollary 3.8: the bilinear large sieve bound restricted to odd numbers

Proved

TaoFivePrimes.large_sieve_odd

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$ , 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|J|/2}\|4j\alpha\|_{\mathbb R/\mathbb Z}}\right)^{1/2}\|a\|_{\ell^{2}(\mathbb Z)}\,\|b\|_{\ell^{2}(\mathbb Z)},

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

This is Corollary 3.7, the bilinear special case of the large sieve inequality, with a factor of two saved in the main term by restricting both variables to odd numbers; the price is that the separation condition is imposed on the multiples of $4\alpha$ rather than of $\alpha$ . It is the form of the large sieve used for the bilinear (Type II) sums of Section 5, and it is the input to the subdivision Corollary 3.9.

Quoted input Corollary 3.7, which the source in turn 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 taken half-open, so that $I\cap\mathbb Z$ is 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|J|/2$ 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_odd (a b : ℤ → ℂ)
    (ha : Summable (fun n : ℤ => ‖a n‖ ^ 2)) (hb : Summable (fun n : ℤ => ‖b n‖ ^ 2))
    (alpha : ℝ) (xI yI xJ yJ : ℝ) (hI : 2 ≤ yI - xI) (hJ : 2 ≤ yJ - xJ)
    (delta : ℝ) (hdelta : 0 < delta)
    (hd : ∀ j : ℤ, 1 ≤ j → (j : ℝ) ≤ (yJ - xJ) / 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)) :
    ‖∑ 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 (∑' 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.8 (Restricting to odd numbers)

View graph