Canonical smooth and rough logarithmic masses of polynomial values

At a zero polynomial value the positive representative is one. This does not change the logarithm, and eventual nonvanishing removes this convention from applications to the product of the original values.

noncomputable def NairTenenbaum.positivePolynomialValue (Q : Polynomial ℤ) (n : ℕ) : ℕ+

The positive absolute polynomial value used in the logarithmic decomposition.

Equations

• NairTenenbaum.positivePolynomialValue Q n = ⟨max 1 (Polynomial.eval (↑n) Q).natAbs, ⋯⟩

theorem NairTenenbaum.positivePolynomialValue_eq {Q : Polynomial ℤ} {n : ℕ} (hn : Polynomial.eval (↑n) Q ≠ 0) : ↑(positivePolynomialValue Q n) = (Polynomial.eval (↑n) Q).natAbs

theorem NairTenenbaum.log_positivePolynomialValue (Q : Polynomial ℤ) (n : ℕ) : Real.log ↑↑(positivePolynomialValue Q n) = Real.log ↑(Polynomial.eval (↑n) Q).natAbs

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

The contribution of smooth prime factors to the logarithmic polynomial mass.

Equations

• NairTenenbaum.polynomialSmoothLogMass Q x y z = ∑ n ∈ NairTenenbaum.shortInterval x y, Real.log ↑↑(NairTenenbaum.smoothPart (NairTenenbaum.positivePolynomialValue Q n) z)

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

The contribution of rough prime factors to the logarithmic polynomial mass.

Equations

• NairTenenbaum.polynomialRoughLogMass Q x y z = ∑ n ∈ NairTenenbaum.shortInterval x y, Real.log ↑↑(NairTenenbaum.roughPart (NairTenenbaum.positivePolynomialValue Q n) z)

theorem NairTenenbaum.polynomialRoughLogMass_eq (Q : Polynomial ℤ) (x y z : ℝ) : polynomialRoughLogMass Q x y z = polynomialLogMass Q x y - polynomialSmoothLogMass Q x y z

theorem NairTenenbaum.polynomialSmoothLogMass_eq_primePower_counts (Q : Polynomial ℤ) (x y : ℝ) {z : ℝ} (hz : 0 ≤ z) (L : ℕ → ℕ) (hL : ∀ p ∈ Finset.filter Nat.Prime (Finset.range (⌊z⌋₊ + 1)), ∀ n ∈ shortInterval x y, (↑(positivePolynomialValue Q n)).factorization p ≤ L p) : polynomialSmoothLogMass Q x y z = ∑ p ∈ Finset.range (⌊z⌋₊ + 1) with Nat.Prime p, (∑ ν ∈ Finset.Icc 1 (L p), ↑{n ∈ shortInterval x y | p ^ ν ∣ ↑(positivePolynomialValue Q n)}.card) * Real.log ↑p

theorem NairTenenbaum.exists_polynomialRoughLogMass_lower_of_smooth_upper {Q : Polynomial ℤ} (hQ : Q ≠ 0) {β : ℝ} (hβ : 0 < β) : ∃ (x₀ : ℝ) (B : ℝ), 1 < x₀ ∧ 0 ≤ B ∧ ∀ (x y z E : ℝ), x₀ < x → x ^ β ≤ y → polynomialSmoothLogMass Q x y z ≤ y * Real.log y + E → ↑Q.natDegree * y * Real.log x - y * Real.log y - (B * y + E) ≤ polynomialRoughLogMass Q x y z

Only the upper bound for the small-prime mass remains to obtain a quantitative lower bound for the rough mass.