Bounds for the Selberg sieve

This file proves a number of results to help bound Sieve.selbergSum

Main Results

• selbergBoundingSum_ge_sum_div: If ν is completely multiplicative then S ≥ ∑_{n ≤ √y}, ν n
• boundingSum_ge_log: If ν n = 1 / n then S ≥ log y / 2
• rem_sum_le_of_const: If R_d ≤ C then the error term is at most C * y * (1 + log y)^3

theorem Sieve.prodDistinctPrimes_squarefree (s : Finset ℕ) (h : ∀ p ∈ s, Nat.Prime p) : Squarefree (∏ p ∈ s, p)

theorem Sieve.primorial_squarefree (n : ℕ) : Squarefree (primorial n)

theorem Sieve.zeta_pos_of_prime (p : ℕ) : Nat.Prime p → 0 < ↑ArithmeticFunction.zeta p

theorem Sieve.zeta_lt_self_of_prime (p : ℕ) : Nat.Prime p → ↑ArithmeticFunction.zeta p < ↑p

theorem Sieve.prime_dvd_primorial_iff (n : ℕ) (p : ℕ) (hp : Nat.Prime p) : p ∣ primorial n ↔ p ≤ n

theorem Sieve.siftedSum_eq (s : SelbergSieve) (hw : ∀ i ∈ s.support, s.weights i = 1) (z : ℝ) (hz : 1 ≤ z) (hP : s.prodPrimes = primorial ⌊z⌋₊) : s.siftedSum = ↑(Finset.filter (fun (d : ℕ) => ∀ (p : ℕ), Nat.Prime p → ↑p ≤ z → ¬p ∣ d) s.support).card

def Sieve.CompletelyMultiplicative (f : ArithmeticFunction ℝ) : Prop

Equations

• Sieve.CompletelyMultiplicative f = (f 1 = 1 ∧ ∀ (a b : ℕ), f (a * b) = f a * f b)

theorem Sieve.CompletelyMultiplicative.zeta : Sieve.CompletelyMultiplicative ↑ArithmeticFunction.zeta

theorem Sieve.CompletelyMultiplicative.id : Sieve.CompletelyMultiplicative ↑ArithmeticFunction.id

theorem Sieve.CompletelyMultiplicative.pmul (f : ArithmeticFunction ℝ) (g : ArithmeticFunction ℝ) (hf : Sieve.CompletelyMultiplicative f) (hg : Sieve.CompletelyMultiplicative g) : Sieve.CompletelyMultiplicative (f.pmul g)

theorem Sieve.CompletelyMultiplicative.pdiv {f : ArithmeticFunction ℝ} {g : ArithmeticFunction ℝ} (hf : Sieve.CompletelyMultiplicative f) (hg : Sieve.CompletelyMultiplicative g) : Sieve.CompletelyMultiplicative (f.pdiv g)

theorem Sieve.CompletelyMultiplicative.isMultiplicative {f : ArithmeticFunction ℝ} (hf : Sieve.CompletelyMultiplicative f) : f.IsMultiplicative

theorem Sieve.CompletelyMultiplicative.apply_pow (f : ArithmeticFunction ℝ) (hf : Sieve.CompletelyMultiplicative f) (a : ℕ) (n : ℕ) : f (a ^ n) = f a ^ n

theorem Sieve.prod_factors_one_div_compMult_ge (M : ℕ) (f : ArithmeticFunction ℝ) (hf : Sieve.CompletelyMultiplicative f) (hf_nonneg : ∀ (n : ℕ), 0 ≤ f n) (d : ℕ) (hd : Squarefree d) (hf_size : ∀ (n : ℕ), Nat.Prime n → n ∣ d → f n < 1) : f d * ∏ p ∈ d.primeFactors, 1 / (1 - f p) ≥ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p ^ n)

theorem Sieve.prod_factors_sum_pow_compMult (M : ℕ) (hM : M ≠ 0) (f : ArithmeticFunction ℝ) (hf : Sieve.CompletelyMultiplicative f) (d : ℕ) (hd : Squarefree d) : ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p ^ n) = ∑ m ∈ Finset.filter (fun (x : ℕ) => d ∣ x) (d ^ M).divisors, f m

theorem Sieve.prod_primes_dvd_of_dvd (P : ℕ) {s : Finset ℕ} (h : ∀ p ∈ s, p ∣ P) (h' : ∀ p ∈ s, Nat.Prime p) : ∏ p ∈ s, p ∣ P

theorem Sieve.sqrt_le_self (x : ℝ) (hx : 1 ≤ x) : √x ≤ x

theorem Sieve.Nat.squarefree_dvd_pow (a : ℕ) (b : ℕ) (N : ℕ) (ha : Squarefree a) (hab : a ∣ b ^ N) : a ∣ b

theorem Sieve.selbergBoundingSum_ge_sum_div (s : SelbergSieve) (hP : ∀ (p : ℕ), Nat.Prime p → ↑p ≤ s.level → p ∣ s.prodPrimes) (hnu : Sieve.CompletelyMultiplicative s.nu) (hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n) (hnu_lt : ∀ (p : ℕ), Nat.Prime p → p ∣ s.prodPrimes → s.nu p < 1) : s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, s.nu m

theorem Sieve.boundingSum_ge_sum (s : SelbergSieve) (hnu : s.nu = (↑ArithmeticFunction.zeta).pdiv ↑ArithmeticFunction.id) (hP : ∀ (p : ℕ), Nat.Prime p → ↑p ≤ s.level → p ∣ s.prodPrimes) : s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√s.level⌋₊, 1 / ↑m

theorem Sieve.boundingSum_ge_log (s : SelbergSieve) (hnu : s.nu = (↑ArithmeticFunction.zeta).pdiv ↑ArithmeticFunction.id) (hP : ∀ (p : ℕ), Nat.Prime p → ↑p ≤ s.level → p ∣ s.prodPrimes) : s.selbergBoundingSum ≥ Real.log s.level / 2

theorem Sieve.rem_sum_le_of_const (s : SelbergSieve) (C : ℝ) (hrem : ∀ d > 0, |s.rem d| ≤ C) : (∑ d ∈ s.prodPrimes.divisors, if ↑d ≤ s.level then 3 ^ ArithmeticFunction.cardDistinctFactors d * |s.rem d| else 0) ≤ C * s.level * (1 + Real.log s.level) ^ 3