LeanPool.SelbergSieve4.Selberg #

source

structure SelbergSieveextends Sieve :

Type

A Selberg sieve is a finite sieve together with a sieve level.

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 : ℝ
Sieve level.
one_le_level : 1 ≤ self.level

Instances For

source

noncomputable def SelbergSieve.selbergBoundingSum (s : SelbergSieve) :

ℝ

Selberg bounding sum over divisors below the square-root level.

Equations

s.selbergBoundingSum = ∑ l ∈ s.prodPrimes.divisors, if ↑(l ^ 2) ≤ s.level then s.selbergTerms l else 0

Instances For

source

theorem SelbergSieve.selbergBoundingSum_pos (s : SelbergSieve) :

0 < s.selbergBoundingSum

source

theorem SelbergSieve.selbergBoundingSum_ne_zero (s : SelbergSieve) :

s.selbergBoundingSum ≠ 0

source

theorem SelbergSieve.selbergBoundingSum_nonneg (s : SelbergSieve) :

0 ≤ s.selbergBoundingSum

source

noncomputable def SelbergSieve.selbergWeights (s : SelbergSieve) :

ℕ → ℝ

Selberg weights attached to the sieve.

Equations

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

Instances For

source

theorem SelbergSieve.selbergWeights_eq_zero_of_not_dvd (s : SelbergSieve) {d : ℕ} (hd : ¬d ∣ s.prodPrimes) :

s.selbergWeights d = 0

source

theorem SelbergSieve.selbergWeights_eq_zero (s : SelbergSieve) (d : ℕ) (hd : ¬↑(d ^ 2) ≤ s.level) :

s.selbergWeights d = 0

source

theorem SelbergSieve.selbergWeights_mul_mu_nonneg (s : SelbergSieve) (d : ℕ) (hdP : d ∣ s.prodPrimes) :

0 ≤ s.selbergWeights d * ↑(ArithmeticFunction.moebius d)

source

theorem SelbergSieve.sum_mul_subst (k n : ℕ) {f : ℕ → ℝ} (h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0) :

∑ l ∈ n.divisors, f l = ∑ m ∈ n.divisors, if k * m ∣ n then f (k * m) else 0

source

theorem SelbergSieve.selbergWeights_eq_dvds_sum (s : SelbergSieve) (d : ℕ) :

s.nu d * s.selbergWeights d = s.selbergBoundingSum⁻¹ * ↑(ArithmeticFunction.moebius d) * ∑ l ∈ s.prodPrimes.divisors, if d ∣ l ∧ ↑(l ^ 2) ≤ s.level then s.selbergTerms l else 0

source

theorem SelbergSieve.selbergWeights_diagonalisation (s : SelbergSieve) (l : ℕ) (hl : l ∈ s.prodPrimes.divisors) :

(∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * s.selbergWeights d else 0) = if ↑(l ^ 2) ≤ s.level then s.selbergTerms l * ↑(ArithmeticFunction.moebius l) * s.selbergBoundingSum⁻¹ else 0

source

noncomputable def SelbergSieve.selbergMuPlus (s : SelbergSieve) :

ℕ → ℝ

Lambda-squared upper-bound weight generated by the Selberg weights.

Equations

s.selbergMuPlus = Sieve.lambdaSquared s.selbergWeights

Instances For

source

theorem SelbergSieve.weight_one_of_selberg (s : SelbergSieve) :

s.selbergWeights 1 = 1

source

theorem SelbergSieve.selbergμPlus_eq_zero (s : SelbergSieve) (d : ℕ) (hd : ¬↑d ≤ s.level) :

s.selbergMuPlus d = 0

source

noncomputable def SelbergSieve.selbergUbSieve (s : SelbergSieve) :

Sieve.UpperBoundSieve

Upper-bound sieve induced by the Selberg weights.

Equations

s.selbergUbSieve = { μPlus := s.selbergMuPlus, hμPlus := ⋯ }

Instances For

source

theorem SelbergSieve.mainSum_eq_diag_quad_form (s : SelbergSieve) :

s.mainSum s.selbergMuPlus = ∑ l ∈ s.prodPrimes.divisors, ↑1 / s.selbergTerms l * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * s.selbergWeights d else 0) ^ 2

source

theorem SelbergSieve.selberg_bound_simple_mainSum (s : SelbergSieve) :

s.mainSum s.selbergMuPlus = s.selbergBoundingSum⁻¹

source

theorem SelbergSieve.eq_gcd_mul_of_dvd_of_coprime {k d m : ℕ} (hkd : k ∣ d) (hmd : m.Coprime d) (hk : k ≠ 0) :

k = d.gcd (k * m)

source

theorem SelbergSieve.selbergBoundingSum_ge (s : SelbergSieve) {d : ℕ} (hdP : d ∣ s.prodPrimes) :

s.selbergBoundingSum ≥ s.selbergWeights d * ↑(ArithmeticFunction.moebius d) * s.selbergBoundingSum

source

theorem SelbergSieve.selberg_bound_weights (s : SelbergSieve) (d : ℕ) :

|s.selbergWeights d| ≤ 1

source

theorem SelbergSieve.selberg_bound_muPlus (s : SelbergSieve) (n : ℕ) (hn : n ∈ s.prodPrimes.divisors) :

|s.selbergMuPlus n| ≤ 3 ^ ArithmeticFunction.cardDistinctFactors n

source

theorem SelbergSieve.selberg_bound_simple_errSum (s : SelbergSieve) :

s.errSum s.selbergMuPlus ≤ ∑ d ∈ s.prodPrimes.divisors, if ↑d ≤ s.level then 3 ^ ArithmeticFunction.cardDistinctFactors d * |s.rem d| else 0

source

theorem SelbergSieve.selberg_bound_simple (s : SelbergSieve) :

s.siftedSum ≤ s.totalMass / s.selbergBoundingSum + ∑ d ∈ s.prodPrimes.divisors, if ↑d ≤ s.level then 3 ^ ArithmeticFunction.cardDistinctFactors d * |s.rem d| else 0