The sharp weighted reciprocal Hooley mean

For an irreducible integer polynomial without a fixed prime divisor, the reciprocal mean has logarithmic exponent 2^t−t and exponential coefficient sqrt(2t)+o(1). The bound includes all positive integers.

noncomputable def NairTenenbaum.hooleySubexponential (η x : ℝ) : ℝ

The subexponential factor used in the sharp weighted Hooley bound.

Equations

• NairTenenbaum.hooleySubexponential η x = Real.exp (η * √(Real.log (Real.log x) * Real.log (Real.log (Real.log x))))

theorem NairTenenbaum.hooleySubexponential_pos (η x : ℝ) : 0 < hooleySubexponential η x

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

theorem NairTenenbaum.exists_hooleyRootSum_X_sharp_bound {η : ℝ} (hη : √2 < η) : ∃ (x₀ : ℝ) (C : ℝ), 1 < x₀ ∧ 0 < C ∧ ∀ (x : ℝ), x₀ < x → hooleyRootSum Polynomial.X 1 x ≤ C * (Real.log x * hooleySubexponential η x)