Summable higher-prime-power tails of the correction

For sufficiently large primes the exponential coefficient bound gives an O(p⁻²) tail. At primes where the linear coefficient vanishes this controls the whole positive-exponent local correction.

theorem NairTenenbaum.rootIdealCorrection_higherPower_tail (K : Type u_1) [Field K] [NumberField K] {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) {p : ℕ} (hp : Nat.Prime p) (hlarge : 2 * rootIdealCorrectionGrowthConstant K Q ≤ ↑p) : (Summable fun (k : ℕ) => |(rootIdealCorrection K Q) (p ^ (k + 2))| / ↑p ^ (k + 2)) ∧ ∑' (k : ℕ), |(rootIdealCorrection K Q) (p ^ (k + 2))| / ↑p ^ (k + 2) ≤ 2 * rootIdealCorrectionGrowthConstant K Q ^ 2 / ↑p ^ 2

theorem NairTenenbaum.rootIdealCorrection_positivePower_tail (K : Type u_1) [Field K] [NumberField K] {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) {p : ℕ} (hp : Nat.Prime p) (hlarge : 2 * rootIdealCorrectionGrowthConstant K Q ≤ ↑p) (hcancel : (rootIdealCorrection K Q) p = 0) : (Summable fun (k : ℕ) => |(rootIdealCorrection K Q) (p ^ (k + 1))| / ↑p ^ (k + 1)) ∧ ∑' (k : ℕ), |(rootIdealCorrection K Q) (p ^ (k + 1))| / ↑p ^ (k + 1) ≤ 2 * rootIdealCorrectionGrowthConstant K Q ^ 2 / ↑p ^ 2