The root-weighted prime step for the Hooley mean

This is the finite form of equation (2.10) in Tenenbaum's weighted mean argument. Its mixed-term constant is explicit. The main weighted prime sum is retained; estimating it sharply is a separate prime-ideal-theorem input.

noncomputable def NairTenenbaum.rootPrimeLogWeight (Q : Polynomial ℤ) (σ : ℝ) (p : ℕ) : ℝ

The prime logarithmic weight multiplied by polynomial root counts.

Equations

• NairTenenbaum.rootPrimeLogWeight Q σ p = ↑(NairTenenbaum.rootCount Q p) * Real.log ↑p / ↑p ^ σ

theorem NairTenenbaum.rootPrimeLogWeight_nonneg (Q : Polynomial ℤ) (σ : ℝ) {p : ℕ} (hp : Nat.Prime p) : 0 ≤ rootPrimeLogWeight Q σ p

theorem NairTenenbaum.rootPrimeLogWeight_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {σ : ℝ} (hσ : 1 ≤ σ) {p : ℕ} (hp : Nat.Prime p) : rootPrimeLogWeight Q σ p ≤ ↑Q.natDegree * (Real.log ↑p / ↑p)

theorem NairTenenbaum.root_weighted_hooleyCrossMoment_le {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (n : ℕ) {q : ℕ} (hq : 1 < q) {σ : ℝ} (hσ : 1 ≤ σ) : ∑ p ∈ S, rootPrimeLogWeight Q σ p * hooleyPrimeCrossMoment q n p ≤ ↑Q.natDegree * (Real.log 4 * Real.exp 2 * 4 ^ q * (↑n.divisors.card ^ (↑q / (↑q - 1)) * hooleyMoment q n ^ ((↑q - 2) / (↑q - 1))))