Divisor hits in the interval prescribed by Theorem 2

This interface uses the original irreducibility and degree hypotheses. The arithmetic root-density lower bound is proved and gives an unconditional divisor-hit estimate in the power-shaped interval.

theorem NairTenenbaum.eventually_power_interval_le_half {β : ℝ} (hβ : β < 1) : ∀ᶠ (x : ℝ) in Filter.atTop, x ^ β ≤ x / 2

theorem NairTenenbaum.exists_theoremTwo_divisorHit_density_bound {Q : Polynomial ℤ} (hQ : Irreducible Q) (hdeg : 0 < Q.natDegree) {k : ℕ} (hk : Q.natDegree < k) {η c : ℝ} (hη : Real.log 4 - 1 < η) (hc : 0 < c) : ∃ (x₀ : ℝ), 1 < x₀ ∧ ∀ (x : ℝ), x₀ < x → have y := x ^ (↑Q.natDegree / ↑k); 4 * c ≤ dyadicRootDensitySum Q y → c * y / Real.log x ^ η ≤ ↑(polynomialDivisorHitCount Q x y)

theorem NairTenenbaum.exists_theoremTwo_divisorHit_bound {Q : Polynomial ℤ} (hQ : Irreducible Q) (hdeg : 0 < Q.natDegree) {k : ℕ} (hk : Q.natDegree < k) {η : ℝ} (hη : Real.log 4 - 1 < η) : ∃ (c : ℝ) (x₀ : ℝ), 0 < c ∧ 1 < x₀ ∧ ∀ (x : ℝ), x₀ < x → have y := x ^ (↑Q.natDegree / ↑k); c * y / Real.log x ^ η ≤ ↑(polynomialDivisorHitCount Q x y)