Divisor bounds and admissibility of Hooley's function

An elementary proof of τ(n) ≤ 2^Ω(n) and τ(n) ≪_ε n^ε. These complete the membership assertion for Δ in the introduction.

theorem NairTenenbaum.succ_le_two_pow (n : ℕ) : n + 1 ≤ 2 ^ n

theorem NairTenenbaum.card_divisors_le_two_pow {n : ℕ} (hn : n ≠ 0) : n.divisors.card ≤ 2 ^ bigOmega n

theorem NairTenenbaum.linear_le_geometric {a : ℝ} (ha : 1 < a) (ν : ℕ) : ↑ν + 1 ≤ (1 + (a - 1)⁻¹) * a ^ ν

A uniform bound for the linear factor in a prime-power divisor count.

theorem NairTenenbaum.primePower_divisor_bound {ε : ℝ} (hε : 0 < ε) (N : ℕ) (hN : 2 ^ ε⁻¹ ≤ ↑N) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : ↑ν + 1 ≤ (if p ≤ N then 1 + (2 ^ ε - 1)⁻¹ else 1) * (↑p ^ ε) ^ ν

theorem NairTenenbaum.exists_card_divisors_le_rpow {ε : ℝ} (hε : 0 < ε) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (n : ℕ), n ≠ 0 → ↑n.divisors.card ≤ B * ↑n ^ ε

The standard subpolynomial divisor bound, with constants uniform in n.

noncomputable def NairTenenbaum.hooleyMap : ArithmeticMap 1

Hooley's function as a function of a one-dimensional positive tuple.

Equations

• NairTenenbaum.hooleyMap n = ↑(NairTenenbaum.hooleyDelta ↑(n 0))

theorem NairTenenbaum.hooley_admissible {ε : ℝ} (hε : 0 < ε) : ∃ (B : ℝ), 1 ≤ B ∧ Admissible 2 B ε hooleyMap

The admissibility assertion in §1, for every positive exponent.

theorem NairTenenbaum.hooley_rpow_admissible {ε t : ℝ} (hε : 0 < ε) (ht : 0 < t) : ∃ (B : ℝ), 1 ≤ B ∧ Admissible (2 ^ t) B ε fun (n : Tuple 1) => hooleyMap n ^ t

Every positive real power of Hooley's function lies in an arithmetic class with an arbitrarily small positive growth exponent.