Counting values divisible by unusually large powers of small primes

theorem NairTenenbaum.polynomialCongruenceCount_le_twice {Q : Polynomial ℤ} {q : ℕ} (hq : 0 < q) {a b : ℤ} (hab : a ≤ b) (hlevel : ↑q ≤ ↑b - ↑a) : ↑(polynomialCongruenceCount Q q a b) ≤ 2 * (↑b - ↑a) * ↑(rootCount Q q) / ↑q

The elementary congruence estimate with the error absorbed by the interval length.

theorem NairTenenbaum.polynomialCongruenceUnion_card_le {ι : Type u_1} (S : Finset ι) (Q : ι → Polynomial ℤ) (q : ι → ℕ) (a b : ℤ) : {t ∈ Finset.Ioc a b | ∃ i ∈ S, ↑(q i) ∣ Polynomial.eval t (Q i)}.card ≤ ∑ i ∈ S, polynomialCongruenceCount (Q i) (q i) a b

A union bound over any finite family of polynomial congruences.

noncomputable def NairTenenbaum.smallPrimes (z : ℝ) : Finset ℕ

The finite set of primes at most the real cutoff.

Equations

• NairTenenbaum.smallPrimes z = Finset.filter Nat.Prime (Finset.range (⌊z⌋₊ + 1))

theorem NairTenenbaum.smallPrimes_le {z : ℝ} (hz : 0 ≤ z) {p : ℕ} (hp : p ∈ smallPrimes z) : ↑p ≤ z

theorem NairTenenbaum.smallPrimes_card_le {z : ℝ} (hz : 1 ≤ z) : ↑(smallPrimes z).card ≤ 2 * z

noncomputable def NairTenenbaum.primePowerExceptionalSet {r : ℕ} (R : Fin r → Polynomial ℤ) (z T : ℝ) (a b : ℤ) : Finset ℤ

Values divisible by a prime power exceeding the threshold for some small prime.

Equations

• NairTenenbaum.primePowerExceptionalSet R z T a b = {t ∈ Finset.Ioc a b | ∃ p ∈ NairTenenbaum.smallPrimes z, ∃ (i : Fin r), ↑p ^ NairTenenbaum.firstPowerAbove p T ∣ Polynomial.eval t (R i)}

theorem NairTenenbaum.primePowerExceptionalSet_card_le {r : ℕ} (R : Fin r → Polynomial ℤ) {z T M : ℝ} (hz : 1 ≤ z) (hT : 1 ≤ T) (hM : 0 ≤ M) (hroot : ∀ p ∈ smallPrimes z, ∀ (i : Fin r), ↑(rootCount (R i) (p ^ firstPowerAbove p T)) ≤ M) {a b : ℤ} (hab : a ≤ b) (hlevel : z * T ≤ ↑b - ↑a) : ↑(primePowerExceptionalSet R z T a b).card ≤ 4 * (↑b - ↑a) * ↑r * M * z / T

The large-prime-power exceptional set has density at most a constant multiple of z/T. This does not assume independence of the coordinates.