Tao Corollary 3.7: the bilinear special case of the large sieve inequality

Proved

TaoFivePrimes.large_sieve_bilinear

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 $1$ , 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\,b_m\,e(nm\alpha)\right| \;\le\;\left(|I|+\frac{1}{\displaystyle\inf_{1\le j\le|J|}\|j\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|$ and $|J|$ are the lengths of the intervals, and $\|t\|_{\mathbb R/\mathbb Z}$ is the distance from $t$ to the nearest integer.

This is the bilinear special case of the large sieve inequality: the frequencies $m\alpha$ , $m\in J\cap\mathbb Z$ , are separated by $\inf_{1\le j\le|J|}\|j\alpha\|$ , and the large sieve applied to that system, combined with Cauchy–Schwarz in the variable $m$ , gives the stated bound. It is the estimate that controls the Type II bilinear sums of Section 5, and it is the input to the odd-restricted Corollary 3.8 and to the subdivision Corollary 3.9.

Quoted input The large sieve inequality itself — for $\xi_1,\dots,\xi_R\in\mathbb R/\mathbb Z$ pairwise separated by $\delta$ and an interval $I$ of length at least $1$ ,

\sum_{i}\Bigl|\sum_{n\in I\cap\mathbb Z}a_n e(\xi_i n)\Bigr|^{2}\le\bigl(|I|+\delta^{-1}\bigr)\|a\|_{\ell^{2}(\mathbb Z)}^{2},

which the source quotes from Montgomery's survey — is not available in the ambient library and appears here as a hypothesis.

Formalization Note Intervals are given by their real endpoints and 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|J|$ is carried as an explicit positive lower bound, which is how the corollary is applied and which avoids a nonemptiness side condition; the distance to the nearest integer is written $|t-\operatorname{round}(t)|$ .

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_Explicit

open Finset

Formal statement

theorem TaoFivePrimes.large_sieve_bilinear (a b : ℤ → ℂ)
    (ha : Summable (fun n : ℤ => ‖a n‖ ^ 2)) (hb : Summable (fun n : ℤ => ‖b n‖ ^ 2))
    (alpha : ℝ) (u1 v1 u2 v2 : ℝ) (hI : 1 ≤ v1 - u1) (hJ : 1 ≤ v2 - u2)
    (delta : ℝ) (hdelta : 0 < delta)
    (hd : ∀ j : ℤ, 1 ≤ j → (j : ℝ) ≤ v2 - u2 →
      delta ≤ |(j : ℝ) * alpha - round ((j : ℝ) * alpha)|)
    (hLS : ∀ (a' : ℤ → ℂ), Summable (fun n : ℤ => ‖a' n‖ ^ 2) →
        ∀ (T : Finset ℤ) (xi : ℤ → ℝ) (d u v : ℝ), 0 < d → 1 ≤ v - u →
        (∀ i ∈ T, ∀ j ∈ T, i ≠ j →
          d ≤ |(xi i - xi j) - round (xi i - xi j)|) →
        (∑ i ∈ T, ‖∑ n ∈ Finset.Ioc ⌊u⌋ ⌊v⌋, a' n * TaoFivePrimes.eR (xi i * (n : ℝ))‖ ^ 2)
          ≤ ((v - u) + 1 / d) * ∑' n : ℤ, ‖a' n‖ ^ 2) :
    ‖∑ n ∈ Finset.Ioc ⌊u1⌋ ⌊v1⌋, ∑ m ∈ Finset.Ioc ⌊u2⌋ ⌊v2⌋,
        a n * b m * TaoFivePrimes.eR (alpha * (n : ℝ) * (m : ℝ))‖
      ≤ Real.sqrt ((v1 - u1) + 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.7 (Special case of large sieve inequality); the quoted large sieve inequality is Lemma 3.6 there, cited to H. L. Montgomery, The analytic principle of the large sieve, Bull. Amer. Math. Soc. 84 (1978), 547-567, Theorem 3

View graph