Euler bound for the squarefree divisor Dirichlet series

The divisor series in the differential inequality is at most the exponential of 2^t times the prime root series. Convergence is proved for σ>1.

noncomputable def NairTenenbaum.rootPrimePowerSum (Q : Polynomial ℤ) (σ : ℝ) : ℝ

The prime Dirichlet series weighted by polynomial root counts.

Equations

• NairTenenbaum.rootPrimePowerSum Q σ = ∑' (p : Nat.Primes), ↑(NairTenenbaum.rootCount Q ↑p) * ↑↑p ^ (-σ)

theorem NairTenenbaum.rootPrimePowerSum_nonneg (Q : Polynomial ℤ) (σ : ℝ) : 0 ≤ rootPrimePowerSum Q σ

theorem NairTenenbaum.summable_rootPrimePowerWeight {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {σ : ℝ} (hσ : 1 < σ) : Summable fun (p : Nat.Primes) => ↑(rootCount Q ↑p) * ↑↑p ^ (-σ)

theorem NairTenenbaum.hooleyDivisorDirichletTerm_eq_primeProduct (Q : Polynomial ℤ) (t σ : ℝ) (n : ℕ) : hooleyMomentCoefficient Q t 1 n * ↑n ^ (-σ) = squarefreePrimeProduct (fun (p : ℕ) => 2 ^ t * ↑(rootCount Q p) * ↑p ^ (-σ)) n

theorem NairTenenbaum.hooleyDivisorDirichlet_le_exp_prime_sum {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (t : ℝ) {σ : ℝ} (hσ : 1 < σ) : hooleyDirichlet Q t 1 σ ≤ Real.exp (2 ^ t * rootPrimePowerSum Q σ)

theorem NairTenenbaum.hooleyDirichlet_le_divisorSeries {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hσ : 1 < σ) : hooleyDirichlet Q t q σ ≤ hooleyDirichlet Q t 1 σ

theorem NairTenenbaum.hooleyDirichlet_le_exp_prime_sum {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (hσ : 1 < σ) : hooleyDirichlet Q t q σ ≤ Real.exp (2 ^ t * rootPrimePowerSum Q σ)