Documentation

LeanPool.NairTenenbaum.Sieve.SelbergDenominator

Quantitative lower bounds for the Selberg denominator #

The logarithmic moment of the full finite Euler product controls the mass lost by truncating the divisor sum. This avoids any asymptotic prime number theorem.

source
theorem NairTenenbaum.powerset_prod_sum_moment {ι : Type u_1} (S : Finset ι) (w v : ι → ℝ) (hw : ∀ p ∈ S, 1 + w p ≠ 0) :
∑ T ∈ S.powerset, (∏ p ∈ T, w p) * ∑ p ∈ T, v p = (∏ p ∈ S, (1 + w p)) * ∑ p ∈ S, w p / (1 + w p) * v p

First moment of an additive statistic under finite product weights.

source
theorem NairTenenbaum.squarefree_divisor_log_moment (f : ArithmeticFunction ℝ) (hf : f.IsMultiplicative) {n : ℕ} (hn : Squarefree n) (hlocal : ∀ p ∈ n.primeFactors, 1 + f p ≠ 0) :
∑ d ∈ n.divisors, f d * Real.log ↑d = (∑ d ∈ n.divisors, f d) * ∑ p ∈ n.primeFactors, f p / (1 + f p) * Real.log ↑p

The logarithm is additive across the distinct prime factors of a squarefree divisor, so its weighted mean is a sum of local means.

source
noncomputable def NairTenenbaum.selbergFullSum (s : BoundingSieve) :
ℝ

The full Selberg denominator sum before truncation.

Equations
Instances For
    source
    theorem NairTenenbaum.selbergFullSum_pos (s : BoundingSieve) :
    0 < selbergFullSum s
    source
    theorem NairTenenbaum.selbergTerms_prime (s : BoundingSieve) {p : ℕ} (hp : Nat.Prime p) :
    BoundingSieve.selbergTerms p = s.nu p / (1 - s.nu p)
    source
    theorem NairTenenbaum.selbergFullSum_euler (s : BoundingSieve) :
    selbergFullSum s = ∏ p ∈ s.prodPrimes.primeFactors, (1 - s.nu p)⁻¹
    source
    theorem NairTenenbaum.selbergFullSum_log_moment (s : BoundingSieve) :
    ∑ d ∈ s.prodPrimes.divisors, BoundingSieve.selbergTerms d * Real.log ↑d = selbergFullSum s * ∑ p ∈ s.prodPrimes.primeFactors, s.nu p * Real.log ↑p
    source
    theorem NairTenenbaum.selbergDenominator_log_tail (s : BoundingSieve) {R : ℝ} (hR : 0 < R) :
    Real.log R * (selbergFullSum s - selbergDenominator s R) ≤ selbergFullSum s * ∑ p ∈ s.prodPrimes.primeFactors, s.nu p * Real.log ↑p

    The logarithmic moment bounds the mass omitted by truncation.

    source
    theorem NairTenenbaum.selbergDenominator_lower (s : BoundingSieve) {R θ : ℝ} (hR : 1 < R) (hmoment : ∑ p ∈ s.prodPrimes.primeFactors, s.nu p * Real.log ↑p ≤ θ * Real.log R) :
    (1 - θ) * selbergFullSum s ≤ selbergDenominator s R

    A relative logarithmic-moment bound retains a fixed fraction of the full Euler product.

    source
    theorem NairTenenbaum.selberg_prime_log_sum_le (s : BoundingSieve) {z g : ℝ} (hz : 2 ≤ z) (hg : 0 ≤ g) (hprimes : ∀ p ∈ s.prodPrimes.primeFactors, ↑p ≤ z) (hdim : ∀ p ∈ s.prodPrimes.primeFactors, s.nu p ≤ g / ↑p) :
    ∑ p ∈ s.prodPrimes.primeFactors, s.nu p * Real.log ↑p ≤ g * (Real.log 4 * (1 + Real.log z))

    The local dimension bound controls the logarithmic moment by an elementary weighted prime sum.

    source
    theorem NairTenenbaum.selbergDenominator_quarter (s : BoundingSieve) {z g : ℝ} (hz : 2 ≤ z) (hzlog : 16 ≤ Real.log z) (hg : 0 < g) (hprimes : ∀ p ∈ s.prodPrimes.primeFactors, ↑p ≤ z) (hdim : ∀ p ∈ s.prodPrimes.primeFactors, s.nu p ≤ g / ↑p) :
    selbergFullSum s / 4 ≤ selbergDenominator s (z ^ (2 * g))

    A cutoff R=z^(2g) retains at least one quarter of the full Euler product once log z≥16. Both constants are independent of the selected sieve primes.

    source
    theorem NairTenenbaum.selbergDenominator_inv_le (s : BoundingSieve) {z g : ℝ} (hz : 2 ≤ z) (hzlog : 16 ≤ Real.log z) (hg : 0 < g) (hprimes : ∀ p ∈ s.prodPrimes.primeFactors, ↑p ≤ z) (hdim : ∀ p ∈ s.prodPrimes.primeFactors, s.nu p ≤ g / ↑p) :
    (selbergDenominator s (z ^ (2 * g)))⁻¹ ≤ 4 * ∏ p ∈ s.prodPrimes.primeFactors, (1 - s.nu p)

    The optimized main sieve coefficient is bounded by four times the sifting Euler product.