Positive tuples of polynomial values and their small-prime divisors #
theorem
NairTenenbaum.PolynomialSystem.substitute_valueTuple
{k r : ℕ}
(P : PolynomialSystem k r)
{a : ℤ}
{n : Tuple r}
(hn : ∀ (i : Fin r), ↑(n i) = (Polynomial.eval a (P.R i)).natAbs)
(j : Fin k)
:
theorem
NairTenenbaum.PolynomialSystem.weightedMass_valueTuple
{k r : ℕ}
(P : PolynomialSystem k r)
{a : ℤ}
{n : Tuple r}
(hn : ∀ (i : Fin r), ↑(n i) = (Polynomial.eval a (P.R i)).natAbs)
:
theorem
NairTenenbaum.PolynomialSystem.pullback_valueTuple
{k r : ℕ}
(P : PolynomialSystem k r)
(F : ArithmeticMap k)
{a : ℤ}
{n : Tuple r}
(hn : ∀ (i : Fin r), ↑(n i) = (Polynomial.eval a (P.R i)).natAbs)
:
pullback P.exponent F n = extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval a (P.Q j)).natAbs
theorem
NairTenenbaum.PolynomialSystem.exists_valueTuple
{k r : ℕ}
(P : PolynomialSystem k r)
{a : ℤ}
(ha : Polynomial.eval a P.total ≠ 0)
:
Nonzero total values supply positive tuples of all irreducible values.
theorem
NairTenenbaum.PolynomialSystem.primeSelect_sieve_coprime
{k r : ℕ}
(P : PolynomialSystem k r)
{a : ℤ}
{n : Tuple r}
(hn : ∀ (i : Fin r), ↑(n i) = (Polynomial.eval a (P.R i)).natAbs)
{q : ℕ}
{z : ℝ}
(hz : 0 ≤ z)
(hq : z < ↑q)
:
(sieveModulus P.total (mass (primeSelect n (Finset.range q))) z).Coprime (Polynomial.eval a P.total).natAbs
A selected prefix satisfies the actual sieve condition whenever its cutoff is larger than the sifting bound.
theorem
NairTenenbaum.PolynomialSystem.sum_roughPrefix_le_of_selected_sum
{k r : ℕ}
(P : PolynomialSystem k r)
{A B σ : ℝ}
{F : ArithmeticMap k}
(hF : Admissible A B σ F)
(hA : 1 ≤ A)
(hB : 0 ≤ B)
(T : Finset ℤ)
(n : ℤ → Tuple r)
(q : ℤ → ℕ)
(hn : ∀ t ∈ T, ∀ (i : Fin r), ↑(n t i) = (Polynomial.eval t (P.R i)).natAbs)
{x α c S : ℝ}
(hx : 1 < x)
(hα : 0 < α)
(hq : ∀ t ∈ T, x ^ α < ↑(q t))
(hvalue : ∀ t ∈ T, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c)
(hselected : ∑ t ∈ T, pullback P.exponent F (primeSelect (n t) (Finset.range (q t))) ≤ S)
:
(∑ t ∈ T, extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs) ≤ A ^ (c / α) * S
Remove rough remainders from a finite sum once the selected-prefix sum is bounded.