A quantitative gap in the Hooley moment exponent

The gap is positive even at t=1. The explicit lower bound is quadratic in the moment order, as needed for optimizing the final bound.

noncomputable def NairTenenbaum.hooleyMomentExponentGap (t : ℝ) (q : ℕ) : ℝ

The exponent gap between the recursive Hooley moment estimates.

Equations

• NairTenenbaum.hooleyMomentExponentGap t q = (2 ^ t - 2 ^ (t / ↑q)) / (↑q - 1) - t / ↑q

theorem NairTenenbaum.two_rpow_le_one_add_six_sevenths {u : ℝ} (hu : 0 ≤ u) (hu₂ : u ≤ 1 / 2) : 2 ^ u ≤ 1 + 6 / 7 * u

theorem NairTenenbaum.hooleyMomentExponentGap_lower {t : ℝ} (ht : 1 ≤ t) {q : ℕ} (hq : 2 < q) (hqt : 2 * t ≤ ↑q) : t / (7 * ↑q * (↑q - 1)) ≤ hooleyMomentExponentGap t q

theorem NairTenenbaum.hooleyMomentExponentGap_pos {t : ℝ} (ht : 1 ≤ t) {q : ℕ} (hq : 2 < q) (hqt : 2 * t ≤ ↑q) : 0 < hooleyMomentExponentGap t q