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 ∈ BoundingSieve.support, BoundingSieve.weights i = 1) (z : ℝ) (hz : 1 ≤ z) (hP : BoundingSieve.prodPrimes = primorial ⌊z⌋₊) : SelbergSieve.siftedSum = ↑{d ∈ BoundingSieve.support | ∀ (p : ℕ), Nat.Prime p → ↑p ≤ z → ¬p ∣ d}.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 : CompletelyMultiplicative ↑ArithmeticFunction.zeta

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

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

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

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

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

theorem Sieve.prod_factors_one_div_compMult_ge (M : ℕ) (f : ArithmeticFunction ℝ) (hf : 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 : CompletelyMultiplicative f) (d : ℕ) (hd : Squarefree d) : ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p ^ n) = ∑ m ∈ {x ∈ (d ^ M).divisors | d ∣ x}, 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 ≤ SelbergSieve.level → p ∣ BoundingSieve.prodPrimes) (hnu : CompletelyMultiplicative BoundingSieve.nu) (hnu_nonneg : ∀ (n : ℕ), 0 ≤ BoundingSieve.nu n) (hnu_lt : ∀ (p : ℕ), Nat.Prime p → p ∣ BoundingSieve.prodPrimes → BoundingSieve.nu p < 1) : s.selbergBoundingSum ≥ ∑ m ∈ Finset.Icc 1 ⌊√SelbergSieve.level⌋₊, BoundingSieve.nu m

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

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

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