LeanPool.SelbergSieve4.SieveLemmas

structure Sieve : Type

Data for a finite weighted sieve problem.

• support : Finset ℕ

  Finite support of integers being sifted.

• prodPrimes : ℕ

  Product of the primes used by the sieve.

• prodPrimes_squarefree : Squarefree self.prodPrimes
• weights : ℕ → ℝ

  Nonnegative weights on the support.

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

  Main term for the weighted support.

• nu : ArithmeticFunction ℝ

  Local density arithmetic function.

• 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

def Sieve.multSum (s : Sieve) (d : ℕ) : ℝ

Weighted count of support elements divisible by d.

Equations

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

def Sieve.rem (s : Sieve) (d : ℕ) : ℝ

Remainder term after subtracting the expected main term from multSum.

Equations

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

def Sieve.siftedSum (s : Sieve) : ℝ

Weighted count of support elements coprime to the sieve modulus.

Equations

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

noncomputable def Sieve.selbergTerms (s : Sieve) : ArithmeticFunction ℝ

Selberg local factor product used in the simple upper-bound sieve.

Equations

• s.selbergTerms = s.nu.pmul (ArithmeticFunction.prodPrimeFactors fun (p : ℕ) => 1 / (1 - s.nu p))

theorem Sieve.selbergTerms_apply (s : Sieve) (d : ℕ) : s.selbergTerms d = s.nu d * ∏ p ∈ d.primeFactors, 1 / (1 - s.nu p)

Expands selbergTerms as a product over the prime factors of d.

def Sieve.mainSum (s : Sieve) (μPlus : ℕ → ℝ) : ℝ

Main contribution of an upper-bound sieve weight.

Equations

• s.mainSum μPlus = ∑ d ∈ s.prodPrimes.divisors, μPlus d * s.nu d

def Sieve.errSum (s : Sieve) (μPlus : ℕ → ℝ) : ℝ

Error contribution of an upper-bound sieve weight.

Equations

• s.errSum μPlus = ∑ d ∈ s.prodPrimes.divisors, |μPlus d| * |s.rem d|

theorem Sieve.prodPrimes_ne_zero (s : Sieve) : s.prodPrimes ≠ 0

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

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

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

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

theorem Sieve.nu_ne_zero_of_mem_divisors_prodPrimes (s : Sieve) {d : ℕ} (hd : d ∈ s.prodPrimes.divisors) : s.nu d ≠ 0

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

def Sieve.delta (n : ℕ) : ℝ

Kronecker delta at 1, valued in the reals.

Equations

• Sieve.delta n = if n = 1 then 1 else 0

theorem Sieve.siftedSum_as_delta (s : Sieve) : s.siftedSum = ∑ d ∈ s.support, s.weights d * delta (s.prodPrimes.gcd d)

theorem Sieve.nu_lt_self_of_dvd_prodPrimes (s : Sieve) (d : ℕ) : d ∣ s.prodPrimes → d ≠ 1 → s.nu d < 1

theorem Sieve.selbergTerms_pos (s : Sieve) (l : ℕ) (hl : l ∣ s.prodPrimes) : 0 < s.selbergTerms l

theorem Sieve.selbergTerms_mult (s : Sieve) : s.selbergTerms.IsMultiplicative

theorem Sieve.one_div_selbergTerms_eq_conv_moebius_nu (s : Sieve) (l : ℕ) (hl : Squarefree l) (hnu_nonzero : s.nu l ≠ 0) : 1 / s.selbergTerms l = ∑ d ∈ l.divisors, ↑(ArithmeticFunction.moebius (l / d)) * (s.nu d)⁻¹

theorem Sieve.nu_eq_conv_one_div_selbergTerms (s : Sieve) (d : ℕ) (hdP : d ∣ s.prodPrimes) : (s.nu d)⁻¹ = ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then 1 / s.selbergTerms l else 0

theorem Sieve.conv_selbergTerms_eq_selbergTerms_mul_nu (s : Sieve) {d : ℕ} (hd : d ∣ s.prodPrimes) : (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then s.selbergTerms l else 0) = s.selbergTerms d * (s.nu d)⁻¹

theorem Sieve.upper_bound_of_UpperBoundSieve (s : Sieve) (μPlus : UpperBoundSieve) : s.siftedSum ≤ ∑ d ∈ s.prodPrimes.divisors, μPlus.μPlus d * s.multSum d

theorem Sieve.siftedSum_le_mainSum_errSum_of_UpperBoundSieve (s : Sieve) (μPlus : UpperBoundSieve) : s.siftedSum ≤ s.totalMass * s.mainSum μPlus.μPlus + s.errSum μPlus.μPlus

def Sieve.lambdaSquared (weights : ℕ → ℝ) : ℕ → ℝ

Lambda-squared upper-bound weights generated from a function on divisors.

Equations

• Sieve.lambdaSquared weights d = ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0

theorem Sieve.lambdaSquared_eq_zero_of_support (w : ℕ → ℝ) (y : ℝ) (hw : ∀ (d : ℕ), ¬↑(d ^ 2) ≤ y → w d = 0) (d : ℕ) (hd : ¬↑d ≤ y) : lambdaSquared w d = 0

theorem Sieve.upperMoebius_of_lambda_sq (weights : ℕ → ℝ) (hw : weights 1 = 1) : UpperMoebius (lambdaSquared weights)

theorem Sieve.lambdaSquared_mainSum_eq_quad_form (s : Sieve) (w : ℕ → ℝ) : s.mainSum (lambdaSquared w) = ∑ d1 ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

theorem Sieve.lambdaSquared_mainSum_eq_diag_quad_form (s : Sieve) (w : ℕ → ℝ) : s.mainSum (lambdaSquared w) = ∑ l ∈ s.prodPrimes.divisors, ↑1 / s.selbergTerms l * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * w d else 0) ^ 2