Summing the repeated-prime contribution

The representation a²b³ proves convergence of Σ n^(−s) on powerful integers for s>1/2. Subpolynomial divisor and root bounds then give the convergent weight τ(n)^t ρ_Q(n)/n needed to remove the squarefree restriction.

theorem NairTenenbaum.summable_powerful_rpow {s : ℝ} (hs : 1 / 2 < s) : Summable fun (n : { n : ℕ // Powerful n }) => ↑↑n ^ (-s)

theorem NairTenenbaum.exists_divisorRootWeight_le_rpow {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {t ε : ℝ} (ht : 0 ≤ t) (hε : 0 < ε) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n : ℕ), n ≠ 0 → ↑n.divisors.card ^ t * ↑(rootCount Q n) ≤ C * ↑n ^ ε

noncomputable def NairTenenbaum.powerfulRootWeight (Q : Polynomial ℤ) (t : ℝ) (n : { n : ℕ // Powerful n }) : ℝ

The root weight restricted to powerful integers.

Equations

• NairTenenbaum.powerfulRootWeight Q t n = ↑(↑n).divisors.card ^ t * ↑(NairTenenbaum.rootCount Q ↑n) / ↑↑n

theorem NairTenenbaum.powerfulRootWeight_nonneg (Q : Polynomial ℤ) (t : ℝ) (n : { n : ℕ // Powerful n }) : 0 ≤ powerfulRootWeight Q t n

theorem NairTenenbaum.summable_powerfulRootWeight {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {t : ℝ} (ht : 0 ≤ t) : Summable (powerfulRootWeight Q t)