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_cube_card_le
{k r : ℕ}
(P : PolynomialSystem k r)
{z : ℝ}
(hz : 1 ≤ z)
{a b : ℤ}
(hab : a ≤ b)
(hlevel : z ^ 4 ≤ ↑b - ↑a)
:
The useful specialization T=z³ produces a quadratic saving.