Montgomery's local $L^2$ concentration bound for the sifted Fourier polynomial

Proved

TaoFivePrimes.montgomery_corollary47_source

by shivm · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorylarge-sievenumber-theorytao-five-primes

For every $x > 1$ , every $R > 1$ and every real weight sequence $w$ , provided the primorial of $\lfloor R\rfloor$ divides the primorial of $\lfloor\sqrt{x}\rfloor$ , the sifted Fourier polynomial obeys the local concentration bound

\int_{\|\alpha\| \le 1/(2R^2)} |S_w(x,\alpha)|^2 \, d\alpha \;\le\; \frac{\log x}{\log R} \sum_{n \le x} \Lambda_{\sqrt{x}\#}(n)\, w(n)^2 ,

where $\Lambda_{\sqrt{x}\#}$ is the sifted von Mangoldt weight and $S_w(x,\cdot)$ the corresponding exponential sum.

This is the $Q = 1$ case of the Montgomery estimate that Tao invokes at Corollary 4.7, and it is one of the large-sieve inputs to the major-arc analysis: it says the $L^2$ mass of the sifted exponential sum near the origin is controlled by the sifted mass of the weights, with a loss of only $\log x / \log R$ .

Provenance note. This statement was previously bundled, in a single platform node, with the unrelated Rosser--Schoenfeld bound $\sum_{n\le x}\Lambda(n) < 1.03883x$ . The two come from different papers and neither depends on the other, so they are separated here to let each be attacked on its own.

Preamble

import Definitions.Def_TaoFivePrimes_ArcSplit
import Mathlib.MeasureTheory.Integral.Bochner.Set

open scoped BigOperators ArithmeticFunction.vonMangoldt
open MeasureTheory

Formal statement

namespace TaoFivePrimes

theorem montgomery_corollary47_source :
    ∀ (x : ℕ) (w : ℕ → ℝ) (R : ℝ),
      1 < x →
      1 < R →
      primorial ⌊R⌋₊ ∣
        primorial (Nat.sqrt x) →
      (∫ α in Metric.closedBall (0 : AddCircle (1 : ℝ))
            (1 / (2 * R ^ 2)),
          ‖TaoFourierIdentity.fourierPolynomial (Finset.range (x + 1))
              (fun n ↦
                ((siftedVonMangoldt x n * w n : ℝ) : ℂ))
              (fun n ↦ (n : ℤ)) α‖ ^ 2
            ∂AddCircle.haarAddCircle) ≤
        (Real.log (x : ℝ) / Real.log R) *
          (∑ n ∈ Finset.range (x + 1),
            siftedVonMangoldt x n * (w n) ^ 2) := by
  sorry

end TaoFivePrimes

Source

Terence Tao, Every odd number greater than 1 is the sum of at most five primes, arXiv:1201.6656v4, Lemma 4.6 and Corollary 4.7 (the Q = 1 case of the Montgomery estimate).

View graph

Montgomery's local L2L^2L2 concentration bound for the sifted Fourier polynomial

Montgomery's local $L^2$ concentration bound for the sifted Fourier polynomial