Hooley moments reduced to their root-weighted means

This is the proved short-sum input to Corollary 4. The long weighted Hooley mean estimate and the sharper polynomial Euler-product estimate used there are separate analytic steps, not hypotheses hidden in the arithmetic class.

theorem NairTenenbaum.extend_hooley_rpow {t : ℝ} (ht : 0 < t) (n : ℕ) : (extendArithmeticMap (fun (v : Tuple 1) => hooleyMap v ^ t) fun (x : Fin 1) => n) = ↑(hooleyDelta n) ^ t

noncomputable def NairTenenbaum.hooleyPolynomialSum (Q : Polynomial ℤ) (t x y : ℝ) : ℝ

The short sum of Hooley's divisor function evaluated on polynomial values.

Equations

• NairTenenbaum.hooleyPolynomialSum Q t x y = ∑ n ∈ NairTenenbaum.shortInterval x y, ↑(NairTenenbaum.hooleyDelta (Polynomial.eval (↑n) Q).natAbs) ^ t

noncomputable def NairTenenbaum.hooleyRootSum (Q : Polynomial ℤ) (t x : ℝ) : ℝ

The root-weighted sum of Hooley's divisor function.

Equations

• NairTenenbaum.hooleyRootSum Q t x = ∑ n ∈ NairTenenbaum.positiveUpTo x, ↑(NairTenenbaum.hooleyDelta ↑n) ^ t * (↑(NairTenenbaum.rootCount Q ↑n) / ↑↑n)

theorem NairTenenbaum.exists_hooleyPolynomialSum_root_bound (Q : Polynomial ℤ) (hQ : NoFixedPrimeDivisor Q) (hdeg : 0 < Q.natDegree) {α t : ℝ} (hα : 0 < α) (ht : 0 < t) : ∃ (x₀ : ℝ) (C : ℝ), 0 < x₀ ∧ 0 < C ∧ ∀ (x y : ℝ), x₀ < x → x ^ α ≤ y → y ≤ x → hooleyPolynomialSum Q t x y ≤ C * (y * sieveProduct Q x * hooleyRootSum Q t x)

The Hooley specialization of the proved main theorem, for every positive interval exponent and moment order. No irreducibility is needed for this root-weighted form. The constants may depend on the fixed polynomial.