Selberg sieve

DefinitionSelberg level set#✓fully proved

For a bounding sieve whose sifting primes have product \(P\) and a natural number \(R\), the level-\(R\) set is the set of divisors \(l\) of \(P\) with \(l \le R\).

def levelSet (s : BoundingSieve) (R : ℕ) : Finset ℕ :=
  s.prodPrimes.divisors.filter fun l ↦ l ≤ R

Used by 10

Used byBrun's theorem on twin primes · Uniform Brun–Titchmarsh bound · Selberg level sum · The Selberg level sum is at least one · Selberg level weights are bounded by one · Main term of the Selberg level weights · Weighted bound for the Selberg level weights · The Selberg level weight at one · Support of the Selberg level weights · Normalized Selberg coefficients

DefinitionSelberg level sum#✓fully proved

For a bounding sieve whose sifting primes have product \(P\), with multiplicative density function \(\nu\), and a natural number \(R\), the level-\(R\) Selberg sum is \(G = \sum_{l \mid P,\ l \le R} g(l)\), where \(g(l) = \nu(l) \prod_{p \mid l} (1 - \nu(p))^{-1}\), the product running over the primes \(p\) dividing \(l\).

noncomputable def levelSum (s : BoundingSieve) (R : ℕ) : ℝ :=
  ∑ l ∈ levelSet s R, s.selbergTerms l

Uses 1 · Used by 9

Statement usesSelberg level set

Used byBrun's theorem on twin primes · Uniform Brun–Titchmarsh bound · The Selberg level sum is at least one · Selberg level weights are bounded by one · Main term of the Selberg level weights · Weighted bound for the Selberg level weights · The Selberg level weight at one · Support of the Selberg level weights · Normalized Selberg coefficients

DefinitionNormalized Selberg coefficients#✓fully proved

Let \(s\) be a bounding sieve with density function \(\nu\) and Selberg terms \(g(l) = \nu(l) \prod_{p \mid l} (1 - \nu(p))^{-1}\), the product running over the primes \(p\) dividing \(l\), and let \(R\) be a natural number. Write \(D_R\) for the level set of \(s\) at level \(R\) (the divisors of the sifting product of \(s\) that are at most \(R\)) and \(G(R) = \sum_{l \in D_R} g(l)\) for the level sum. The normalized Selberg coefficient of \(s\) at level \(R\) is the function on natural numbers given by \(y_l = \mu(l)\, g(l) / G(R)\) for \(l \in D_R\) and \(y_l = 0\) otherwise, where \(\mu\) is the Möbius function.

noncomputable def levelY
    (s : BoundingSieve) (R l : ℕ) : ℝ :=
  if l ∈ levelSet s R then
    ((ArithmeticFunction.moebius l : ℤ) : ℝ) * s.selbergTerms l /
      levelSum s R
  else 0

Uses 2 · Used by 8

Statement usesSelberg level set · Selberg level sum

Used bySelberg sieve weights · Selberg level weights are bounded by one · Error bound for the Selberg level weights · Inversion formula for the Selberg level weights · Main term of the Selberg level weights · Weighted bound for the Selberg level weights · The Selberg level weight at one · Support of the Selberg level weights

DefinitionSelberg sieve weights#✓fully proved

Let \(s\) be a bounding sieve with sifting product \(P\) (the product of its sifting primes) and density function \(\nu\), let \(R\) be a natural number, and let \(y_m\) denote the normalized Selberg coefficients of \(s\) at level \(R\). For a natural number \(d\), the level-\(R\) Selberg weight of \(s\) at \(d\) is

\[\lambda_d = \nu(d)^{-1} \sum_{m \mid P,\ d \mid m} \mu(m/d)\, y_m,\]

where \(\mu\) is the Möbius function, \(m\) runs over the divisors of \(P\), and \(\nu(d)^{-1}\) is read as \(0\) when \(\nu(d) = 0\).

noncomputable def levelWeights
    (s : BoundingSieve) (R d : ℕ) : ℝ :=
  (s.nu d)⁻¹ * ∑ m ∈ s.prodPrimes.divisors,
    if d ∣ m then ((ArithmeticFunction.moebius (m / d) : ℤ) : ℝ) *
      levelY s R m else 0

Uses 1 · Used by 9

Statement usesNormalized Selberg coefficients

Used byBrun's theorem on twin primes · Uniform Brun–Titchmarsh bound · Selberg level weights are bounded by one · Error bound for the Selberg level weights · Inversion formula for the Selberg level weights · Main term of the Selberg level weights · Weighted bound for the Selberg level weights · The Selberg level weight at one · Support of the Selberg level weights

TheoremThe Selberg level sum is at least one#✓fully proved

For every bounding sieve and every natural number \(R \ge 1\), the level-\(R\) Selberg sum is at least \(1\).

theorem levelSum_ge_one (s : BoundingSieve) (R : ℕ)
    (hR : 1 ≤ R) : 1 ≤ levelSum s R

Uses 2 · Used by 5

Statement usesSelberg level sum

Proof usesSelberg level set

Used byBrun's theorem on twin primes · Selberg level weights are bounded by one · Main term of the Selberg level weights · Weighted bound for the Selberg level weights · The Selberg level weight at one

TheoremInversion formula for the Selberg level weights#✓fully proved

For a bounding sieve whose sifting primes have product \(P\), with density function \(\nu\), a natural number \(R\) and a divisor \(l\) of \(P\), the level-\(R\) Selberg weights \(\lambda_d\) satisfy \(\sum_{d \mid P,\ l \mid d} \nu(d)\,\lambda_d = y_l\), where \(y_l\) is the normalized level-\(R\) Selberg \(y\)-coefficient at \(l\).

theorem levelWeights_inner (s : BoundingSieve) (R l : ℕ)
    (hl : l ∣ s.prodPrimes) :
    (∑ d ∈ s.prodPrimes.divisors,
      if l ∣ d then s.nu d * levelWeights s R d else 0) =
      levelY s R l

Uses 2 · Used by 1

Statement usesSelberg sieve weights · Normalized Selberg coefficients

Used byMain term of the Selberg level weights

TheoremThe Selberg level weight at one#✓fully proved

For every bounding sieve and every natural number \(R \ge 1\), the level-\(R\) Selberg weight at \(1\) equals \(1\).

theorem levelWeights_one (s : BoundingSieve) (R : ℕ)
    (hR : 1 ≤ R) : levelWeights s R 1 = 1

Uses 5 · Used by 2

Statement usesSelberg sieve weights

Proof usesSelberg level set · Selberg level sum · The Selberg level sum is at least one · Normalized Selberg coefficients

Used byBrun's theorem on twin primes · Uniform Brun–Titchmarsh bound

TheoremMain term of the Selberg level weights#✓fully proved

For a bounding sieve whose sifting primes have product \(P\), with density function \(\nu\), and a natural number \(R \ge 1\), let \(\lambda_d\) be the level-\(R\) Selberg weights and \(\Lambda_d = \sum_{d_1, d_2 \mid d,\ \operatorname{lcm}(d_1, d_2) = d} \lambda_{d_1} \lambda_{d_2}\) their \(\Lambda^2\) coefficients. Then \(\sum_{d \mid P} \Lambda_d\,\nu(d) = 1/G\), where \(G\) is the level-\(R\) Selberg sum.

theorem levelWeights_mainSum (s : BoundingSieve) (R : ℕ)
    (hR : 1 ≤ R) :
    s.mainSum (BoundingSieve.lambdaSquared (levelWeights s R)) =
      1 / levelSum s R

Uses 6 · Used by 2

Statement usesSelberg level sum · Selberg sieve weights

Proof usesSelberg level set · The Selberg level sum is at least one · Inversion formula for the Selberg level weights · Normalized Selberg coefficients

Used byBrun's theorem on twin primes · Uniform Brun–Titchmarsh bound

TheoremWeighted bound for the Selberg level weights#✓fully proved

For a bounding sieve whose sifting primes have product \(P\), with density function \(\nu\), a natural number \(R \ge 1\) and a divisor \(d\) of \(P\), the level-\(R\) Selberg weight \(\lambda_d\) at \(d\) satisfies \(|\nu(d)\,\lambda_d| \le 1\).

theorem levelWeights_nu_mul_abs_le
    (s : BoundingSieve) (R d : ℕ) (hR : 1 ≤ R) (hd : d ∣ s.prodPrimes) :
    |s.nu d * levelWeights s R d| ≤ 1

Uses 5 · Used by 1

Statement usesSelberg sieve weights

Proof usesSelberg level set · Selberg level sum · The Selberg level sum is at least one · Normalized Selberg coefficients

Used byError bound for the Selberg level weights

TheoremSelberg level weights are bounded by one#✓fully proved

For a bounding sieve whose sifting primes have product \(P\), a natural number \(R \ge 1\) and a divisor \(d\) of \(P\), the level-\(R\) Selberg weight \(\lambda_d\) at \(d\) satisfies \(|\lambda_d| \le 1\).

theorem levelWeights_abs_le
    (s : BoundingSieve) (R d : ℕ) (hR : 1 ≤ R) (hd : d ∣ s.prodPrimes) :
    |levelWeights s R d| ≤ 1

Uses 5

Statement usesSelberg sieve weights

Proof usesSelberg level set · Selberg level sum · The Selberg level sum is at least one · Normalized Selberg coefficients

TheoremSupport of the Selberg level weights#✓fully proved

For every bounding sieve and all natural numbers \(R\) and \(d\), if the level-\(R\) Selberg weight \(\lambda_d\) at \(d\) is nonzero, then \(d \le R\).

theorem levelWeights_support
    (s : BoundingSieve) (R d : ℕ)
    (hd : levelWeights s R d ≠ 0) : d ≤ R

Uses 4 · Used by 1

Statement usesSelberg sieve weights

Proof usesSelberg level set · Selberg level sum · Normalized Selberg coefficients

Used byError bound for the Selberg level weights

TheoremError bound for the Selberg level weights#✓fully proved

Take a bounding sieve whose sifting primes have product \(P\), with density function \(\nu\) and remainders \(r_d = A_d - \nu(d) X\), where \(A_d\) is the total weight of the multiples of \(d\) in the set to be sifted and \(X\) approximates its total weight. Let \(R \ge 1\) be a natural number and suppose that \(d\,\nu(d) \ge 1\) and \(|r_d| \le d\) for every divisor \(d\) of \(P\). Let \(\lambda_d\) be the level-\(R\) Selberg weights and \(\Lambda_d = \sum_{d_1, d_2 \mid d,\ \operatorname{lcm}(d_1, d_2) = d} \lambda_{d_1} \lambda_{d_2}\) their \(\Lambda^2\) coefficients. Then \(\sum_{d \mid P} |\Lambda_d|\,|r_d| \le R^{12}\).

theorem levelWeights_errSum_le
    (s : BoundingSieve) (R : ℕ) (hR : 1 ≤ R)
    (hnu : ∀ d : ℕ, d ∣ s.prodPrimes → 1 ≤ (d : ℝ) * s.nu d)
    (hrem : ∀ d : ℕ, d ∣ s.prodPrimes → |s.rem d| ≤ (d : ℝ)) :
    s.errSum (BoundingSieve.lambdaSquared (levelWeights s R)) ≤
      (R : ℝ) ^ 12

Uses 4 · Used by 2

Statement usesSelberg sieve weights

Proof usesWeighted bound for the Selberg level weights · Support of the Selberg level weights · Normalized Selberg coefficients

Used byBrun's theorem on twin primes · Uniform Brun–Titchmarsh bound

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.