Divisor hits without a restriction on fixed prime divisors

The analytic tail estimate covers fixed prime divisors. The final implication keeps its numerical root-density lower bound explicit; that arithmetic estimate is a separate remaining input to Theorem 2.

theorem NairTenenbaum.exists_divisorWindow_rootDensity_le_hits_add_small_unrestricted {Q : Polynomial ℤ} (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {α η c : ℝ} (hα : 0 < α) (hη : Real.log 4 - 1 < η) (hc : 0 < c) : ∃ (x₀ : ℝ), 1 < x₀ ∧ ∀ (x y : ℝ), x₀ < x → x ^ α ≤ y → y ≤ x / 2 → y / 2 * dyadicRootDensitySum Q y ≤ Real.log x ^ η * ↑(polynomialDivisorHitCount Q x y) + c * y

theorem NairTenenbaum.exists_polynomialDivisorHitCount_density_bound_unrestricted {Q : Polynomial ℤ} (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {α η c : ℝ} (hα : 0 < α) (hη : Real.log 4 - 1 < η) (hc : 0 < c) : ∃ (x₀ : ℝ), 1 < x₀ ∧ ∀ (x y : ℝ), x₀ < x → x ^ α ≤ y → y ≤ x / 2 → 4 * c ≤ dyadicRootDensitySum Q y → c * y / Real.log x ^ η ≤ ↑(polynomialDivisorHitCount Q x y)