An elementary tenth-moment divisor bound

For the paper's preliminary all-divisors route, the generic factorization constant in ExplicitDivisorBound.lean is much too large. Here each prime factor is charged a small power-of-two penalty. The penalties over primes below 1024 sum exactly to 447; primes at least 1024 need no penalty.

def BGS.NumberTheory.preliminaryPrimePenalty (p : ℕ) : ℕ

Power-of-two penalty assigned to a prime factor. The thresholds are the first primes at which the optimal integer penalty decreases.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.NumberTheory.card_divisors_pow_ten_le_preliminary_constant_mul (n : ℕ) (hn : n ≠ 0) : n.divisors.card ^ 10 ≤ 2 ^ 447 * n

The divisor function satisfies the uniform elementary estimate τ(n)^10 ≤ 2^447 n.