Tao Lemma 3.6: the large sieve inequality

Disproved

TaoFivePrimes.large_sieve_inequality

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

analytic-number-theorylarge-sievenumber-theory

Montgomery's large sieve inequality. Let $(a_n)_{n\in\mathbb Z}$ be square-summable, let $u<v$ with $v-u\ge1$ , let $T$ be a finite set and $(\xi_i)_{i\in T}$ real numbers that are $\delta$ -separated modulo $1$ , that is

\|\xi_i-\xi_j\|_{\mathbb R/\mathbb Z}\ \ge\ \delta\qquad(i\ne j\text{ in }T)

for some $\delta>0$ . Then

\sum_{i\in T}\Bigl|\sum_{u<n\le v}a_n\,e(\xi_i n)\Bigr|^2\ \le\ \Bigl((v-u)+\frac1\delta\Bigr)\sum_{n\in\mathbb Z}|a_n|^2 .

This is the large sieve inequality in the sharp form of Montgomery and Vaughan and of Selberg, quoted by the source as its Lemma 3.6. It is the analytic engine of the minor-arc treatment: the bilinear special case (the source's Corollary 3.7) and its subdivision form (Corollary 3.9) both reduce to it, and through them so does the Type II estimate of Section 5. The constant $(v-u)+\frac1\delta$ is best possible in the sense that neither summand can be reduced.

Formalization Note The sum over $n$ is taken over $(\lfloor u\rfloor,\lfloor v\rfloor]$ , which is the set of integers in $(u,v]$ , and $e(\theta)=e^{2\pi i\theta}$ is the platform's TaoFivePrimes.eR. The separation is stated through round, so that $|t-\mathrm{round}\,t|$ is the distance from $t$ to the nearest integer. This is exactly the shape consumed as a hypothesis by TaoFivePrimes.large_sieve_bilinear.

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_Explicit

open Finset

Formal statement

theorem TaoFivePrimes.large_sieve_inequality
    (a : ℤ → ℂ) (ha : Summable (fun n : ℤ => ‖a n‖ ^ 2))
    (T : Finset ℤ) (xi : ℤ → ℝ) (d u v : ℝ) (hd : 0 < d) (huv : 1 ≤ v - u)
    (hsep : ∀ 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 := 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, Lemma 3.6, quoted from H. L. Montgomery and R. C. Vaughan, "The large sieve", Mathematika 20 (1973), 119-134

View graph