Corollary 4: short sums of powers of Hooley's function

For every t≥1, the logarithmic exponent is 2^t−t−1 and the subexponential coefficient is every number greater than sqrt(2t).

theorem NairTenenbaum.exists_hooleyPolynomialSum_sharp_bound {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {t ε η : ℝ} (ht : 1 ≤ t) (hε : 0 < ε) (hη : √(2 * t) < η) : ∃ (x₀ : ℝ) (C : ℝ), 1 < x₀ ∧ 0 < C ∧ ∀ (x y : ℝ), x₀ < x → x ^ ε ≤ y → y ≤ x → hooleyPolynomialSum Q t x y ≤ C * (y * Real.log x ^ (2 ^ t - t - 1) * hooleySubexponential η x)

def NairTenenbaum.CorollaryFour : Prop

The statement of Corollary 4, with the scope recorded in the source alignment.

Equations

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

theorem NairTenenbaum.corollaryFour : CorollaryFour