Counting polynomial values with a large smooth divisor

noncomputable def NairTenenbaum.smoothLargeDivisors (s : Finset ℕ) (N : ℕ+) (T : ℝ) : Finset ℕ+

Smooth divisors between the lower real cutoff and the upper integral cutoff.

Equations

• NairTenenbaum.smoothLargeDivisors s N T = {n ∈ Finset.Icc 1 N | ↑n ∈ Nat.factoredNumbers s ∧ T < ↑↑n}

noncomputable def NairTenenbaum.smoothDivisorExceptionalSet (Q : Polynomial ℤ) (s : Finset ℕ) (N : ℕ+) (T : ℝ) (a b : ℤ) : Finset ℤ

Polynomial values divisible by one of the specified large smooth divisors.

Equations

• NairTenenbaum.smoothDivisorExceptionalSet Q s N T a b = {t ∈ Finset.Ioc a b | ∃ d ∈ NairTenenbaum.smoothLargeDivisors s N T, ↑↑d ∣ Polynomial.eval t Q}

noncomputable def NairTenenbaum.smoothDivisorBound (g D : ℕ) (s : Finset ℕ) : ℝ

The uniform constant for counting values with a large smooth divisor.

Equations

• NairTenenbaum.smoothDivisorBound g D s = ↑(max g (D ^ 3) ^ (Finset.filter Nat.Prime s).card) * (1 / (1 - 2 ^ (-(1 / 2)))) ^ (Finset.filter Nat.Prime s).card

theorem NairTenenbaum.smoothDivisorBound_pos (g : ℕ) {D : ℕ} (hD : 0 < D) (s : Finset ℕ) : 0 < smoothDivisorBound g D s

theorem NairTenenbaum.PolynomialSystem.smoothDivisorExceptionalSet_card_le {k r : ℕ} (P : PolynomialSystem k r) (s : Finset ℕ) (N : ℕ+) {T : ℝ} (hT : 0 < T) {a b : ℤ} (hab : a ≤ b) (hlevel : ↑↑N ≤ ↑b - ↑a) : ↑(smoothDivisorExceptionalSet P.radical s N T a b).card ≤ 2 * (↑b - ↑a) * smoothDivisorBound P.total.natDegree P.badDiscriminant s * T ^ (-(1 / 2))

A union over the large smooth moduli uses their reciprocal-density tail.

theorem NairTenenbaum.PolynomialSystem.weightedMass_le_tupleLCM_pow {k r : ℕ} (P : PolynomialSystem k r) (m : Tuple r) : weightedMass P.exponent m ≤ tupleLCM m ^ P.total.natDegree

The least common multiple of the coordinates controls their weighted mass with exponent at most the total polynomial degree.

theorem NairTenenbaum.PolynomialSystem.mem_smoothDivisorExceptionalSet_of_tuple {k r : ℕ} (P : PolynomialSystem k r) (s : Finset ℕ) (N : ℕ+) {T : ℝ} {a b t : ℤ} (ht : t ∈ Finset.Ioc a b) (m : Tuple r) (hdiv : ∀ (i : Fin r), ↑↑(m i) ∣ Polynomial.eval t (P.R i)) (hsmooth : weightedMass P.exponent m ∈ Nat.factoredNumbers s) (hlarge : T ^ P.total.natDegree < ↑(weightedMass P.exponent m)) (hsmall : weightedMass P.exponent m ≤ ↑N) : t ∈ smoothDivisorExceptionalSet P.radical s N T a b

A large smooth divisor tuple gives a single large smooth divisor of the radical value, even when its coordinates have common prime factors.