Documentation

PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg

The Selberg Sieve #

This file proves selberg_bound_simple, the main theorem of the Selberg.

def SelbergSieve.selbergBoundingSum (s : SelbergSieve) :

Equations

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

Instances For

theorem SelbergSieve.selbergBoundingSum_pos (s : SelbergSieve) :

0 < s.selbergBoundingSum

theorem SelbergSieve.selbergBoundingSum_ne_zero (s : SelbergSieve) :

s.selbergBoundingSum ≠ 0

theorem SelbergSieve.selbergBoundingSum_nonneg (s : SelbergSieve) :

0 ≤ s.selbergBoundingSum

def SelbergSieve.selbergWeights (s : SelbergSieve) :

Equations

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

Instances For

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

s.selbergWeights d = 0

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

s.selbergWeights d = 0

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

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

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

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

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

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

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

def SelbergSieve.selbergMuPlus (s : SelbergSieve) :

Equations

s.selbergMuPlus = SelbergSieve.lambdaSquared s.selbergWeights

Instances For

theorem SelbergSieve.weight_one_of_selberg (s : SelbergSieve) :

s.selbergWeights 1 = 1

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

s.selbergMuPlus d = 0

def SelbergSieve.selbergUbSieve (s : SelbergSieve) :

UpperBoundSieve

Equations

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

Instances For

theorem SelbergSieve.mainSum_eq_diag_quad_form (s : SelbergSieve) :

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

theorem SelbergSieve.selberg_bound_simple_mainSum (s : SelbergSieve) :

mainSum s.selbergMuPlus = s.selbergBoundingSum⁻¹

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)

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

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

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

|s.selbergWeights d| ≤ 1

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

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

theorem SelbergSieve.selberg_bound_simple_errSum (s : SelbergSieve) :

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

theorem SelbergSieve.selberg_bound_simple (s : SelbergSieve) :

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