Positivity of the global convolution correction

theorem NairTenenbaum.rootIdealCorrection_sum_pos_of_absolute_convergence (K : Type u_1) [Field K] [NumberField K] (Q : Polynomial ℤ) (habs : Summable fun (n : ℕ) => |(rootIdealCorrection K Q) n| / ↑n) (htails : Summable fun (p : ℕ) => if Nat.Prime p then ∑' (k : ℕ), |(rootIdealCorrection K Q) (p ^ (k + 1))| / ↑p ^ (k + 1) else 0) : 0 < ∑' (n : ℕ), (rootIdealCorrection K Q) n / ↑n