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

References

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

structure 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 self.prodPrimes
• weights : ℕ → ℝ

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

• weights_nonneg (n : ℕ) : 0 ≤ self.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 : self.nu.IsMultiplicative
• nu_pos_of_prime (p : ℕ) : Nat.Prime p → p ∣ self.prodPrimes → 0 < self.nu p
• nu_lt_one_of_prime (p : ℕ) : Nat.Prime p → p ∣ self.prodPrimes → self.nu p < 1

structure 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 self.prodPrimes
• weights : ℕ → ℝ
• weights_nonneg (n : ℕ) : 0 ≤ self.weights n
• totalMass : ℝ
• nu : ArithmeticFunction ℝ
• nu_mult : self.nu.IsMultiplicative
• nu_pos_of_prime (p : ℕ) : Nat.Prime p → p ∣ self.prodPrimes → 0 < self.nu p
• nu_lt_one_of_prime (p : ℕ) : Nat.Prime p → p ∣ self.prodPrimes → self.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 ≤ self.level

def Mathlib.Meta.Positivity.evalBoundingSieveWeights : PositivityExt

Extension for the positivity tactic: BoundingSieve.weights.

Equations

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

theorem BoundingSieve.one_le_y {s : SelbergSieve} : 1 ≤ s.level

Lemmas about $P$.

theorem BoundingSieve.prodPrimes_ne_zero {s : BoundingSieve} : s.prodPrimes ≠ 0

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

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

Lemmas about $\nu$.

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

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

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

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

def BoundingSieve.multSum {s : BoundingSieve} (d : ℕ) : ℝ

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

Equations

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

def BoundingSieve.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

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

def BoundingSieve.siftedSum {s : BoundingSieve} : ℝ

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

Equations

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

def BoundingSieve.mainSum {s : BoundingSieve} (muPlus : ℕ → ℝ) : ℝ

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

Equations

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

def BoundingSieve.errSum {s : BoundingSieve} (muPlus : ℕ → ℝ) : ℝ

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

Equations

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

theorem BoundingSieve.multSum_eq_main_err {s : BoundingSieve} (d : ℕ) : multSum d = s.nu d * s.totalMass + rem d

theorem BoundingSieve.siftedSum_eq_sum_support_mul_ite {s : BoundingSieve} : siftedSum = ∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0

@[deprecated BoundingSieve.siftedSum_eq_sum_support_mul_ite (since := "2025-07-27")]

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

Alias of BoundingSieve.siftedSum_eq_sum_support_mul_ite.

def BoundingSieve.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

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

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

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