Root-density and remainder terms for the small-prime logarithmic mass

noncomputable def NairTenenbaum.smoothLogRootMain (Q : Polynomial ℤ) (z : ℝ) (L : ℕ → ℕ) : ℝ

The main term of the logarithmically weighted smooth-root count.

Equations

• NairTenenbaum.smoothLogRootMain Q z L = ∑ p ∈ Finset.range (⌊z⌋₊ + 1) with Nat.Prime p, (∑ ν ∈ Finset.Icc 1 (L p), ↑(NairTenenbaum.rootCount Q (p ^ ν)) / ↑p ^ ν) * Real.log ↑p

noncomputable def NairTenenbaum.smoothLogRootError (Q : Polynomial ℤ) (z : ℝ) (L : ℕ → ℕ) : ℝ

The remainder in the logarithmically weighted smooth-root count.

Equations

• NairTenenbaum.smoothLogRootError Q z L = ∑ p ∈ Finset.range (⌊z⌋₊ + 1) with Nat.Prime p, (∑ ν ∈ Finset.Icc 1 (L p), ↑(NairTenenbaum.rootCount Q (p ^ ν))) * Real.log ↑p

theorem NairTenenbaum.polynomialSmoothLogMass_le_root_terms (Q : Polynomial ℤ) {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) (hQ : ∀ n ∈ shortInterval x y, Polynomial.eval (↑n) Q ≠ 0) (L : ℕ → ℕ) (hL : ∀ p ∈ Finset.filter Nat.Prime (Finset.range (⌊z⌋₊ + 1)), ∀ n ∈ shortInterval x y, (Polynomial.eval (↑n) Q).natAbs.factorization p ≤ L p) : polynomialSmoothLogMass Q x y z ≤ (y + 1) * smoothLogRootMain Q z L + smoothLogRootError Q z L