The dyadic root-density lower bound for irreducible polynomials

Integral normalization identifies prime root counts with prime-norm ideal counts away from finitely many primes. The correction theorem then gives a positive mean for the squarefree root counts of the original polynomial.

theorem NairTenenbaum.exists_primitive_irreducible_squarefreeRoot_mean {Q : Polynomial ℤ} (hprim : Q.IsPrimitive) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) : ∃ (L : ℝ), 0 < L ∧ Filter.Tendsto (fun (x : ℝ) => arithmeticSummatory (⇑(squarefreeRootArithmetic Q)) x / x) Filter.atTop (nhds L)

theorem NairTenenbaum.exists_irreducible_squarefreeRoot_mean {Q : Polynomial ℤ} (hQ : Irreducible Q) (hdeg : 0 < Q.natDegree) : ∃ (L : ℝ), 0 < L ∧ Filter.Tendsto (fun (x : ℝ) => arithmeticSummatory (⇑(squarefreeRootArithmetic Q)) x / x) Filter.atTop (nhds L)

theorem NairTenenbaum.exists_irreducible_dyadicRootDensity_lower_bound {Q : Polynomial ℤ} (hQ : Irreducible Q) (hdeg : 0 < Q.natDegree) : ∃ (c : ℝ), 0 < c ∧ ∀ᶠ (y : ℝ) in Filter.atTop, c ≤ dyadicRootDensitySum Q y