The Selberg Sieve

We set up the working assumptions of the Selberg sieve, define the notion of an upper bound sieve and show that every upper bound sieve yields an upper bound on the size of the sifted set. We also define the Λ² sieve and prove that Λ² sieves are upper bound sieves. We then diagonalise the main term of the Λ² sieve.

We mostly follow the treatment outlined by Heath-Brown in the notes to an old graduate course. One minor notational difference is that we write $\nu(n)$ in place of $\frac{\omega(n)}{n}$.

Results

• siftedSum_le_mainSum_errSum_of_UpperBoundSieve - Every upper bound sieve gives an upper bound on the size of the sifted set in terms of mainSum and errSum

Notation

The SelbergSieve.Notation namespace includes common shorthand for the variables included in the SelbergSieve structure.

• A for support
• 𝒜 d for multSum d - the combined weight of the elements of A that are divisible by d
• P for prodPrimes
• a for weights
• X for totalMass
• ν for nu
• y for level
• R d for rem d
• g d for selbergTerms d

References

• Heath-Brown, Lectures on sieves
• Koukoulopoulos, The Distribution of Prime Numbers

class BoundingSieve : Type

We set up a sieve problem as follows. Take a finite set of natural numbers A, whose elements are weighted by a sequence a n. Also take a finite set of primes P, represented by a squarefree natural number. These are the primes that we will sift from our set A. Suppose we can approximate ∑ n ∈ {k ∈ A | d ∣ k}, a n = ν d * X + R d, where X is an approximation to the total size of A and ν is a multiplicative arithmetic function such that 0 < ν p < 1 for all primes p ∣ P.

Then a sieve-type theorem will give us an upper (or lower) bound on the size of the sifted sum ∑ n ∈ {k ∈ support | k.Coprime P}, a n, obtained by removing any elements of A that are a multiple of a prime in P.

• support : Finset ℕ

  The set of natural numbers that is to be sifted. The fundamental lemma yields an upper bound on the size of this set after the multiples of small primes have been removed.

• prodPrimes : ℕ

  The finite set of prime numbers whose multiples are to be sifted from support. We work with their product because it lets us treat nu as a multiplicative arithmetic function. It also plays well with Moebius inversion.

• prodPrimes_squarefree : Squarefree prodPrimes
• weights : ℕ → ℝ

  A sequence representing how much each element of support should be weighted.

• weights_nonneg (n : ℕ) : 0 ≤ weights n
• totalMass : ℝ

  An approximation to ∑ i in support, weights i, i.e. the size of the unsifted set. A bad approximation will yield a weak statement in the final theorem.

• nu : ArithmeticFunction ℝ

  nu d is an approximation to the proportion of elements of support that are a multiple of d

• nu_mult : nu.IsMultiplicative
• nu_pos_of_prime (p : ℕ) : Nat.Prime p → p ∣ prodPrimes → 0 < nu p
• nu_lt_one_of_prime (p : ℕ) : Nat.Prime p → p ∣ prodPrimes → nu p < 1

class SelbergSieveextends BoundingSieve : Type

The Selberg upper bound sieve in particular introduces a parameter called the level which gives the user control over the size of the error term.

• support : Finset ℕ
• prodPrimes : ℕ
• prodPrimes_squarefree : Squarefree prodPrimes
• weights : ℕ → ℝ
• weights_nonneg (n : ℕ) : 0 ≤ weights n
• totalMass : ℝ
• nu : ArithmeticFunction ℝ
• nu_mult : nu.IsMultiplicative
• nu_pos_of_prime (p : ℕ) : Nat.Prime p → p ∣ prodPrimes → 0 < nu p
• nu_lt_one_of_prime (p : ℕ) : Nat.Prime p → p ∣ prodPrimes → nu p < 1
• level : ℝ

  The level of the sieve controls how many terms we include in the inclusion-exclusion type sum. A higher level will yield a tighter bound for the main term, but will also increase the size of the error term.

• one_le_level : 1 ≤ level

def SelbergSieve.Notation.termν : Lean.ParserDescr

nu d is an approximation to the proportion of elements of support that are a multiple of d

Equations

• SelbergSieve.Notation.termν = Lean.ParserDescr.node `SelbergSieve.Notation.termν 1024 (Lean.ParserDescr.symbol "ν")

def SelbergSieve.Notation.termν.«delab_app.BoundingSieve.nu» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def SelbergSieve.Notation.termP.«delab_app.BoundingSieve.prodPrimes» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def SelbergSieve.Notation.termP : Lean.ParserDescr

The finite set of prime numbers whose multiples are to be sifted from support. We work with their product because it lets us treat nu as a multiplicative arithmetic function. It also plays well with Moebius inversion.

Equations

• SelbergSieve.Notation.termP = Lean.ParserDescr.node `SelbergSieve.Notation.termP 1024 (Lean.ParserDescr.symbol "P")

def SelbergSieve.Notation.termA.«delab_app.BoundingSieve.weights» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def SelbergSieve.Notation.termA : Lean.ParserDescr

A sequence representing how much each element of support should be weighted.

Equations

• SelbergSieve.Notation.termA = Lean.ParserDescr.node `SelbergSieve.Notation.termA 1024 (Lean.ParserDescr.symbol "a")

def SelbergSieve.Notation.termX.«delab_app.BoundingSieve.totalMass» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def SelbergSieve.Notation.termX : Lean.ParserDescr

An approximation to ∑ i in support, weights i, i.e. the size of the unsifted set. A bad approximation will yield a weak statement in the final theorem.

Equations

• SelbergSieve.Notation.termX = Lean.ParserDescr.node `SelbergSieve.Notation.termX 1024 (Lean.ParserDescr.symbol "X")

def SelbergSieve.Notation.termA_1 : Lean.ParserDescr

The set of natural numbers that is to be sifted. The fundamental lemma yields an upper bound on the size of this set after the multiples of small primes have been removed.

Equations

• SelbergSieve.Notation.termA_1 = Lean.ParserDescr.node `SelbergSieve.Notation.termA_1 1024 (Lean.ParserDescr.symbol "A")

def SelbergSieve.Notation.termA_1.«delab_app.BoundingSieve.support» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def SelbergSieve.Notation.termY : Lean.ParserDescr

The level of the sieve controls how many terms we include in the inclusion-exclusion type sum. A higher level will yield a tighter bound for the main term, but will also increase the size of the error term.

Equations

• SelbergSieve.Notation.termY = Lean.ParserDescr.node `SelbergSieve.Notation.termY 1024 (Lean.ParserDescr.symbol "y")

def SelbergSieve.Notation.termY.«delab_app.SelbergSieve.level» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

theorem SelbergSieve.Notation.one_le_y [s : SelbergSieve] : 1 ≤ level

Lemmas about $P$.

theorem SelbergSieve.prodPrimes_ne_zero [s : BoundingSieve] : BoundingSieve.prodPrimes ≠ 0

theorem SelbergSieve.squarefree_of_dvd_prodPrimes [s : BoundingSieve] {d : ℕ} (hd : d ∣ BoundingSieve.prodPrimes) : Squarefree d

theorem SelbergSieve.squarefree_of_mem_divisors_prodPrimes [s : BoundingSieve] {d : ℕ} (hd : d ∈ BoundingSieve.prodPrimes.divisors) : Squarefree d

Lemmas about $\nu$.

theorem SelbergSieve.prod_primeFactors_nu [s : BoundingSieve] {d : ℕ} (hd : d ∣ BoundingSieve.prodPrimes) : ∏ p ∈ d.primeFactors, BoundingSieve.nu p = BoundingSieve.nu d

theorem SelbergSieve.nu_pos_of_dvd_prodPrimes [s : BoundingSieve] {d : ℕ} (hd : d ∣ BoundingSieve.prodPrimes) : 0 < BoundingSieve.nu d

theorem SelbergSieve.nu_ne_zero [s : BoundingSieve] {d : ℕ} (hd : d ∣ BoundingSieve.prodPrimes) : BoundingSieve.nu d ≠ 0

theorem SelbergSieve.nu_lt_one_of_dvd_prodPrimes [s : BoundingSieve] {d : ℕ} (hdP : d ∣ BoundingSieve.prodPrimes) (hd_ne_one : d ≠ 1) : BoundingSieve.nu d < 1

def SelbergSieve.multSum [s : BoundingSieve] (d : ℕ) : ℝ

The weight of all the elements that are a multiple of d.

Equations

• SelbergSieve.multSum d = ∑ n ∈ BoundingSieve.support, if d ∣ n then BoundingSieve.weights n else 0

def SelbergSieve.Notation.term𝒜.«delab_app.SelbergSieve.multSum» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def SelbergSieve.Notation.term𝒜 : Lean.ParserDescr

The weight of all the elements that are a multiple of d.

Equations

• SelbergSieve.Notation.term𝒜 = Lean.ParserDescr.node `SelbergSieve.Notation.term𝒜 1024 (Lean.ParserDescr.symbol "𝒜")

def SelbergSieve.rem [s : BoundingSieve] (d : ℕ) : ℝ

The remainder term in the approximation A_d = ν (d) X + R_d. This is the degree to which nu fails to approximate the proportion of the weight that is a multiple of d.

Equations

• SelbergSieve.rem d = SelbergSieve.multSum d - BoundingSieve.nu d * BoundingSieve.totalMass

def SelbergSieve.Notation.termR.«delab_app.SelbergSieve.rem» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def SelbergSieve.Notation.termR : Lean.ParserDescr

The remainder term in the approximation A_d = ν (d) X + R_d. This is the degree to which nu fails to approximate the proportion of the weight that is a multiple of d.

Equations

• SelbergSieve.Notation.termR = Lean.ParserDescr.node `SelbergSieve.Notation.termR 1024 (Lean.ParserDescr.symbol "R")

def SelbergSieve.siftedSum [s : BoundingSieve] : ℝ

The weight of all the elements that are not a multiple of any of our finite set of primes.

Equations

• SelbergSieve.siftedSum = ∑ d ∈ BoundingSieve.support, if BoundingSieve.prodPrimes.Coprime d then BoundingSieve.weights d else 0

def SelbergSieve.mainSum [s : BoundingSieve] (muPlus : ℕ → ℝ) : ℝ

X * mainSum μ⁺ is the main term in the upper bound on sifted_sum.

Equations

• SelbergSieve.mainSum muPlus = ∑ d ∈ BoundingSieve.prodPrimes.divisors, muPlus d * BoundingSieve.nu d

def SelbergSieve.errSum [s : BoundingSieve] (muPlus : ℕ → ℝ) : ℝ

errSum μ⁺ is the error term in the upper bound on sifted_sum.

Equations

• SelbergSieve.errSum muPlus = ∑ d ∈ BoundingSieve.prodPrimes.divisors, |muPlus d| * |SelbergSieve.rem d|

theorem SelbergSieve.multSum_eq_main_err [s : BoundingSieve] (d : ℕ) : multSum d = BoundingSieve.nu d * BoundingSieve.totalMass + rem d

theorem SelbergSieve.siftedsum_eq_sum_support_mul_ite [s : BoundingSieve] : siftedSum = ∑ d ∈ BoundingSieve.support, BoundingSieve.weights d * if BoundingSieve.prodPrimes.gcd d = 1 then 1 else 0

def SelbergSieve.IsUpperMoebius (muPlus : ℕ → ℝ) : Prop

A sequence of coefficients $\mu^{+}$ is upper Moebius if $\mu * \zeta ≤ \mu^{+} * \zeta$. These coefficients then yield an upper bound on the sifted sum.

Equations

• SelbergSieve.IsUpperMoebius muPlus = ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d

theorem SelbergSieve.siftedSum_le_sum_of_upperMoebius [s : BoundingSieve] (muPlus : ℕ → ℝ) (h : IsUpperMoebius muPlus) : siftedSum ≤ ∑ d ∈ BoundingSieve.prodPrimes.divisors, muPlus d * multSum d

theorem SelbergSieve.siftedSum_le_mainSum_errSum_of_upperMoebius [s : BoundingSieve] (muPlus : ℕ → ℝ) (h : IsUpperMoebius muPlus) : siftedSum ≤ BoundingSieve.totalMass * mainSum muPlus + errSum muPlus