Quantitative lower logarithmic mass of polynomial values

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

The sum of logarithms of absolute polynomial values on a short interval.

Equations

• NairTenenbaum.polynomialLogMass Q x y = ∑ n ∈ NairTenenbaum.shortInterval x y, Real.log ↑(Polynomial.eval (↑n) Q).natAbs

theorem NairTenenbaum.exists_power_le_mul_eval_natAbs {Q : Polynomial ℤ} (hQ : Q ≠ 0) : ∃ (x₀ : ℝ) (C : ℝ), 1 < x₀ ∧ 0 < C ∧ ∀ (n : ℕ), x₀ < ↑n → ↑n ^ Q.natDegree ≤ C * ↑(Polynomial.eval (↑n) Q).natAbs

theorem NairTenenbaum.exists_polynomial_eval_log_lower_bound {Q : Polynomial ℤ} (hQ : Q ≠ 0) : ∃ (x₀ : ℝ) (B : ℝ), 1 < x₀ ∧ 0 ≤ B ∧ ∀ (n : ℕ), x₀ < ↑n → Polynomial.eval (↑n) Q ≠ 0 ∧ ↑Q.natDegree * Real.log ↑n - B ≤ Real.log ↑(Polynomial.eval (↑n) Q).natAbs

theorem NairTenenbaum.exists_polynomialLogMass_card_lower_bound {Q : Polynomial ℤ} (hQ : Q ≠ 0) : ∃ (x₀ : ℝ) (B : ℝ), 1 < x₀ ∧ 0 ≤ B ∧ ∀ (x y : ℝ), x₀ < x → ↑(shortInterval x y).card * (↑Q.natDegree * Real.log x - B) ≤ polynomialLogMass Q x y