The sharp squarefree reciprocal Hooley mean

For every η>sqrt(2t), the reciprocal sum over squarefree integers is O((log x)^(2^t−t) exp(η sqrt(log₂ x log₃ x))). The integer moment order is chosen by a proved asymptotic optimization.

theorem NairTenenbaum.momentPower_eq_log_cost {K t x : ℝ} {q : ℕ} (hKq : 0 < K * ↑q) (hx : 1 < x) : (K * ↑q) ^ q * Real.log x ^ (2 ^ t - t + t / ↑q) = Real.log x ^ (2 ^ t - t) * Real.exp (↑q * Real.log (K * ↑q) + t * Real.log (Real.log x) / ↑q)

theorem NairTenenbaum.eventually_squarefreeHooleyRootSum_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {t η : ℝ} (ht : 1 ≤ t) (hη : √(2 * t) < η) : ∀ᶠ (x : ℝ) in Filter.atTop, squarefreeHooleyRootSum Q t x ≤ 2 ^ t * Real.exp 1 * (Real.log x ^ (2 ^ t - t) * Real.exp (η * √(Real.log (Real.log x) * Real.log (Real.log (Real.log x)))))

theorem NairTenenbaum.exists_squarefreeHooleyRootSum_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 → squarefreeHooleyRootSum Q t x ≤ C * (Real.log x ^ (2 ^ t - t) * Real.exp (η * √(Real.log (Real.log x) * Real.log (Real.log (Real.log x)))))