Choosing a Hooley moment that gives logarithmic tail saving

theorem NairTenenbaum.exists_hooley_tail_exponent {η : ℝ} (hη : Real.log 4 - 1 < η) : ∃ (ε : ℝ), 0 < ε ∧ 2 ^ (1 + ε) - (1 + ε) - 1 - ε * η < 0

theorem NairTenenbaum.tendsto_sqrt_mul_log_div_self : Filter.Tendsto (fun (u : ℝ) => √(u * Real.log u) / u) Filter.atTop (nhds 0)

theorem NairTenenbaum.eventually_hooleySubexponential_le_log_rpow (η : ℝ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (x : ℝ) in Filter.atTop, hooleySubexponential η x ≤ Real.log x ^ δ