Statement of Theorem 2

This file defines the target proposition; it does not assert a proof. The polynomial is explicitly nonconstant. The integer k is fixed before choosing the threshold, as in the proof in the paper. No restriction on fixed prime divisors is imposed.

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

The product of the polynomial values in the interval of Theorem 2.

Equations

• NairTenenbaum.polynomialValueProduct Q x y = ∏ n ∈ NairTenenbaum.shortInterval x y, (Polynomial.eval (↑n) Q).natAbs

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

The greatest prime factor of the polynomial-value product.

Equations

• NairTenenbaum.polynomialGreatestPrimeFactor Q x y = (NairTenenbaum.polynomialValueProduct Q x y).maxPrimeFac

def NairTenenbaum.TheoremTwo : Prop

Theorem 2 with positive degree and the fixed divisor-window parameter.

Equations

• One or more equations did not get rendered due to their size.