Comparison between the maximum and integral moments

The maximum window is covered by two adjacent windows. Integrating this cover over one unit of translation proves the lower half of (2.6) in the weighted Hooley mean argument, with the sharp factor 2^(q-1) used there.

theorem NairTenenbaum.divisorWindow_le_adjacent (n : ℕ) {u v : ℝ} (hv₀ : u - 1 ≤ v) (hvu : v ≤ u) : divisorWindow n u ≤ divisorWindow n v + divisorWindow n (v + 1)

theorem NairTenenbaum.hooleyWindow_pow_le_localIntegral (n : ℕ) {q : ℕ} (hq : 0 < q) (u : ℝ) : hooleyWindow n u ^ q ≤ 2 ^ (q - 1) * ∫ (v : ℝ) in u - 1..u + 1, hooleyWindow n v ^ q

A window value is bounded by the moment on its two-unit neighborhood.

theorem NairTenenbaum.hooleyDelta_pow_le_moment (n : ℕ) {q : ℕ} (hq : 0 < q) : ↑(hooleyDelta n) ^ q ≤ 2 ^ (q - 1) * hooleyMoment q n

Each maximum window is bounded by the integral moment. This argument also handles the zero integer and does not assume the maximum is unique.

theorem NairTenenbaum.card_divisors_le_hooleyMoment (n : ℕ) {q : ℕ} (hq : 0 < q) : ↑n.divisors.card ≤ hooleyMoment q n

theorem NairTenenbaum.hooleyMoment_pos {n q : ℕ} (hn : n ≠ 0) (hq : 0 < q) : 0 < hooleyMoment q n