Summing the mixed error in the Dirichlet series

Hölder interpolation keeps the moment series in the error term, instead of replacing it by a divisor bound. This is the nonlinear term needed in the differential inequality.

noncomputable def NairTenenbaum.hooleyPrimeErrorConstant (Q : Polynomial ℤ) (q : ℕ) : ℝ

A uniform constant controlling the prime-step error for Hooley moments.

Equations

• NairTenenbaum.hooleyPrimeErrorConstant Q q = ↑Q.natDegree * (Real.log 4 * Real.exp 2 * 4 ^ q)

theorem NairTenenbaum.hooleyPrimeErrorConstant_nonneg (Q : Polynomial ℤ) (q : ℕ) : 0 ≤ hooleyPrimeErrorConstant Q q

theorem NairTenenbaum.hooleyPrimeErrorBound_factor (Q : Polynomial ℤ) (q n : ℕ) : hooleyPrimeErrorBound Q q n = hooleyPrimeErrorConstant Q q * (↑n.divisors.card ^ (↑q / (↑q - 1)) * hooleyMoment q n ^ ((↑q - 2) / (↑q - 1)))

theorem NairTenenbaum.weighted_moment_error_factor {C T M w r : ℝ} (hC : 0 ≤ C) (hT : 0 ≤ T) (hM : 0 ≤ M) (hw : 0 ≤ w) (hr : 1 < r) (t : ℝ) : w * (C * (T ^ (r / (r - 1)) * M ^ ((r - 2) / (r - 1)))) ^ (t / r) = C ^ (t / r) * (T ^ t * w) ^ (1 / (r - 1)) * (M ^ (t / r) * w) ^ (1 - 1 / (r - 1))

noncomputable def NairTenenbaum.hooleyErrorDirichletTerm (Q : Polynomial ℤ) (t : ℝ) (q : ℕ) (σ : ℝ) (n : ℕ) : ℝ

The Dirichlet-series term contributed by the Hooley prime-step error.

Equations

• NairTenenbaum.hooleyErrorDirichletTerm Q t q σ n = if Squarefree n then ↑(NairTenenbaum.rootCount Q n) * ↑n ^ (-σ) * NairTenenbaum.hooleyPrimeErrorBound Q q n ^ (t / ↑q) else 0

theorem NairTenenbaum.hooleyErrorDirichletTerm_factor (Q : Polynomial ℤ) (t σ : ℝ) {q : ℕ} (hq : 2 < q) (n : ℕ) : hooleyErrorDirichletTerm Q t q σ n = hooleyPrimeErrorConstant Q q ^ (t / ↑q) * (hooleyMomentCoefficient Q t 1 n * ↑n ^ (-σ)) ^ (1 / (↑q - 1)) * (hooleyMomentCoefficient Q t q n * ↑n ^ (-σ)) ^ (1 - 1 / (↑q - 1))

theorem NairTenenbaum.summable_and_hooleyErrorDirichlet_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t σ : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 2 < q) (hσ : 1 < σ) : Summable (hooleyErrorDirichletTerm Q t q σ) ∧ ∑' (n : ℕ), hooleyErrorDirichletTerm Q t q σ n ≤ hooleyPrimeErrorConstant Q q ^ (t / ↑q) * hooleyDirichlet Q t 1 σ ^ (1 / (↑q - 1)) * hooleyDirichlet Q t q σ ^ (1 - 1 / (↑q - 1))