LeanPool.SelbergSieve4.Selberg

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 : ℝ

  The level of the sieve controls how many terms we include in the inclusion-exclusion type sum. A higher level will yield a tighter bound for the main term, but will also increase the size of the error term.

• level : ℝ

  Sieve level.

• one_le_level : 1 ≤ self.level
• one_le_level : 1 ≤ self.level

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

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

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.

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

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

theorem SelbergSieve.selbergWeights_mul_mu_nonneg (s : SelbergSieve) (d : ℕ) (hdP : d ∣ s.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 : ℕ) : 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

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

noncomputable def SelbergSieve.selbergMuPlus (s : SelbergSieve) : ℕ → ℝ

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

Equations

• s.selbergMuPlus = Sieve.lambdaSquared s.selbergWeights

theorem SelbergSieve.weight_one_of_selberg (s : SelbergSieve) : s.selbergWeights 1 = 1

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

noncomputable def SelbergSieve.selbergUbSieve (s : SelbergSieve) : Sieve.UpperBoundSieve

Upper-bound sieve induced by the Selberg weights.

Equations

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

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

theorem SelbergSieve.selberg_bound_simple_mainSum (s : SelbergSieve) : s.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 ∣ s.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 ∈ s.prodPrimes.divisors) : |s.selbergMuPlus n| ≤ 3 ^ ArithmeticFunction.cardDistinctFactors n

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

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