Positive root density from eventual prime-norm agreement

theorem NairTenenbaum.rootIdealCorrection_prime_tails_summable_of_eventual_match (K : Type u_1) [Field K] [NumberField K] {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) (N : ℕ) (hmatch : ∀ (p : ℕ), Nat.Prime p → N < p → rootCount Q p = idealNormCount K p) : Summable fun (p : ℕ) => if Nat.Prime p then ∑' (k : ℕ), |(rootIdealCorrection K Q) (p ^ (k + 1))| / ↑p ^ (k + 1) else 0

theorem NairTenenbaum.rootIdealCorrection_abs_summable_of_eventual_match (K : Type u_1) [Field K] [NumberField K] {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) (N : ℕ) (hmatch : ∀ (p : ℕ), Nat.Prime p → N < p → rootCount Q p = idealNormCount K p) : Summable fun (n : ℕ) => |(rootIdealCorrection K Q) n| / ↑n

theorem NairTenenbaum.exists_squarefreeRoot_mean_of_eventual_ideal_match (K : Type u_1) [Field K] [NumberField K] {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) (N : ℕ) (hmatch : ∀ (p : ℕ), Nat.Prime p → N < p → rootCount Q p = idealNormCount K p) : ∃ (L : ℝ), 0 < L ∧ Filter.Tendsto (fun (x : ℝ) => arithmeticSummatory (⇑(squarefreeRootArithmetic Q)) x / x) Filter.atTop (nhds L)