Documentation

LeanPool.NairTenenbaum.Contributions.SecondContributionCounting

The second class lies in the large-prime-power exceptional set #

theorem NairTenenbaum.PolynomialSystem.mem_primePowerExceptionalSet_of_crossing {k r : ℕ} (P : PolynomialSystem k r) {a b t : ℤ} (ht : t ∈ Finset.Ioc a b) {n : Tuple r} (hn : ∀ (i : Fin r), ↑(n i) = (Polynomial.eval t (P.R i)).natAbs) {p : ℕ} (hp : Nat.Prime p) {z T : ℝ} (hz : 0 ≤ z) (hpz : ↑p ≤ z) (hT : 1 ≤ T) (hsmall : ↑(weightedMass P.exponent (primeSelect n (Finset.range p))) ≤ T ^ P.total.natDegree) (hcross : (T ^ P.total.natDegree) ^ 2 < ↑(weightedMass P.exponent (primeSelect n (Finset.range (p + 1))))) :
theorem NairTenenbaum.PolynomialSystem.primePowerExceptionalSet_card_le {k r : ℕ} (P : PolynomialSystem k r) {z T : ℝ} (hz : 1 ≤ z) (hT : 1 ≤ T) {a b : ℤ} (hab : a ≤ b) (hlevel : z * T ≤ ↑b - ↑a) :
↑(primePowerExceptionalSet P.R z T a b).card ≤ 4 * (↑b - ↑a) * ↑P.total.natDegree * ↑(max P.total.natDegree (P.badDiscriminant ^ 3)) * z / T

The root-count constant depends only on the total degree and restricted bad discriminant.

theorem NairTenenbaum.PolynomialSystem.primePowerExceptionalSet_cube_card_le {k r : ℕ} (P : PolynomialSystem k r) {z : ℝ} (hz : 1 ≤ z) {a b : ℤ} (hab : a ≤ b) (hlevel : z ^ 4 ≤ ↑b - ↑a) :
↑(primePowerExceptionalSet P.R z (z ^ 3) a b).card ≤ 4 * (↑b - ↑a) * ↑P.total.natDegree * ↑(max P.total.natDegree (P.badDiscriminant ^ 3)) / z ^ 2

The useful specialization T=z³ produces a quadratic saving.