A weighted joint divisor bound for neighboring integers

The weighted divisor estimate τ(n)^20 ≤ 2^796 n^2 retains substantially more information than the square of the tenth-moment bound. For the neighboring even integers p - 1 and p + 1, their exact gcd-two identity also controls the product of their divisor counts. Splitting into balanced and dominant cases then gives a twentieth moment for their sum whose leading constant is still 2^796.

theorem BGS.NumberTheory.card_divisors_pred_mul_card_divisors_succ_pow_twenty_le {p : ℕ} (hp : Odd p) (hpTwo : 2 < p) : ((p - 1).divisors.card * (p + 1).divisors.card) ^ 20 ≤ 2 ^ 814 * (p ^ 2 - 1) ^ 2

The product of the two neighboring divisor counts has only one weighted prime-penalty factor in its twentieth moment.

theorem BGS.NumberTheory.card_divisors_pred_mul_card_divisors_succ_pow_ten_weighted_le {p : ℕ} (hp : Odd p) (hpTwo : 2 < p) : ((p - 1).divisors.card * (p + 1).divisors.card) ^ 10 ≤ 2 ^ 407 * p ^ 2

Square-root form of the weighted joint product moment.

def BGS.NumberTheory.neighboringDivisorSumWeightedMomentConstant : ℕ

Joint weighted twentieth-moment constant for the sum of the neighboring divisor counts.

Equations

• BGS.NumberTheory.neighboringDivisorSumWeightedMomentConstant = 2 ^ 796 + 2 ^ 781

theorem BGS.NumberTheory.neighboringDivisorSumWeightedMomentConstant_eq : neighboringDivisorSumWeightedMomentConstant = 2 ^ 781 * 32769

theorem BGS.NumberTheory.card_divisors_pred_add_card_divisors_succ_pow_twenty_le {p : ℕ} (hp : Odd p) (hpLarge : 794039 ≤ p) : ((p - 1).divisors.card + (p + 1).divisors.card) ^ 20 ≤ neighboringDivisorSumWeightedMomentConstant * p ^ 2

Weighted joint twentieth moment for the sum of the neighboring divisor counts. Comparable counts are controlled by their product; a dominant count is controlled by its individual weighted moment.