Double counting polynomial divisors in a dyadic window

theorem NairTenenbaum.dyadicDivisorCount_eq_congruence_filter {n : ℕ} (hn : n ≠ 0) {y : ℝ} (hy : 0 ≤ y) : dyadicDivisorCount n y = {d ∈ shortInterval (y / 2) (y / 2) | d ∣ n}.card

theorem NairTenenbaum.polynomialDivisorWindowSum_eq_congruence_sum (Q : Polynomial ℤ) {x y : ℝ} (hy : 0 ≤ y) (hQ : ∀ n ∈ shortInterval x y, Polynomial.eval (↑n) Q ≠ 0) : polynomialDivisorWindowSum Q x y = ∑ d ∈ shortInterval (y / 2) (y / 2), ↑{n ∈ shortInterval x y | d ∣ (Polynomial.eval (↑n) Q).natAbs}.card

theorem NairTenenbaum.polynomialDivisorWindowSum_ge_rootCount_sum (Q : Polynomial ℤ) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 < y) (hQ : ∀ n ∈ shortInterval x y, Polynomial.eval (↑n) Q ≠ 0) : ∑ d ∈ shortInterval (y / 2) (y / 2), ↑(rootCount Q d) ≤ polynomialDivisorWindowSum Q x y

noncomputable def NairTenenbaum.dyadicRootDensitySum (Q : Polynomial ℤ) (y : ℝ) : ℝ

The sum of root densities over the dyadic interval above half the cutoff.

Equations

• NairTenenbaum.dyadicRootDensitySum Q y = ∑ d ∈ NairTenenbaum.shortInterval (y / 2) (y / 2), ↑(NairTenenbaum.rootCount Q d) / ↑d

theorem NairTenenbaum.polynomialDivisorWindowSum_ge_rootDensity (Q : Polynomial ℤ) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 < y) (hQ : ∀ n ∈ shortInterval x y, Polynomial.eval (↑n) Q ≠ 0) : y / 2 * dyadicRootDensitySum Q y ≤ polynomialDivisorWindowSum Q x y

theorem NairTenenbaum.exists_polynomial_eval_nonzero_on_shortInterval {Q : Polynomial ℤ} (hQ : Q ≠ 0) : ∃ (x₀ : ℝ), 0 ≤ x₀ ∧ ∀ (x y : ℝ), x₀ < x → ∀ n ∈ shortInterval x y, Polynomial.eval (↑n) Q ≠ 0