Small polynomial divisor sums in the original tuple variables

Whole-prime-power splitting reindexes the original divisor tuples into good and bad parts. Tuples with zero congruence count contribute zero; all remaining tuples inherit the required discriminant coprimality from an actual value.

theorem NairTenenbaum.mass_dvd_weightedMass {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (m : Tuple r) : mass m ∣ weightedMass γ m

theorem NairTenenbaum.mass_badSieveModuli_le_weightedMass {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (u v : Tuple r) : mass (badSieveModuli u v) ≤ weightedMass γ (u * v)

theorem NairTenenbaum.prime_dvd_mass_iff_tupleLCM {r : ℕ} (u : Tuple r) {p : ℕ} (hp : Nat.Prime p) : p ∣ mass u ↔ p ∣ tupleLCM u

theorem NairTenenbaum.sieveModulus_badSieveModuli {r : ℕ} (Q : Polynomial ℤ) (u v : Tuple r) (z : ℝ) : sieveModulus Q (mass (badSieveModuli u v)) z = sieveModulus Q (mass (u * v)) z

noncomputable def NairTenenbaum.smallDivisorTuples {k r : ℕ} (γ : Fin k → Fin r → ℕ) (N : ℕ+) : Finset (Tuple r)

Divisor tuples whose weighted mass is at most the cutoff.

Equations

• NairTenenbaum.smallDivisorTuples γ N = {m ∈ NairTenenbaum.tupleBox r N | NairTenenbaum.weightedMass γ m ≤ ↑N}

noncomputable def NairTenenbaum.smallBadParts {k r : ℕ} (γ : Fin k → Fin r → ℕ) (D : ℕ) (v : Tuple r) (N : ℕ+) : Finset (Tuple r)

Bad-prime-supported tuples whose product with the good part has bounded weighted mass.

Equations

• NairTenenbaum.smallBadParts γ D v N = {u ∈ NairTenenbaum.tupleBox r N | (∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers D.primeFactors) ∧ NairTenenbaum.weightedMass γ (u * v) ≤ ↑N}

theorem NairTenenbaum.mem_smallBadParts {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (u v : Tuple r) (N : ℕ+) : u ∈ smallBadParts γ D v N ↔ (∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers D.primeFactors) ∧ weightedMass γ (u * v) ≤ ↑N

noncomputable def NairTenenbaum.PolynomialSystem.smallDivisorSiftedSum {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (N : ℕ+) (a b : ℤ) (z : ℝ) : ℝ

Weighted count of sifted polynomial values over all small divisor tuples.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.PolynomialSystem.smallDivisor_split_mem {k r : ℕ} (P : PolynomialSystem k r) (N : ℕ+) (m : Tuple r) (hm : m ∈ smallDivisorTuples P.exponent N) (n : ℤ) (hdiv : ∀ (i : Fin r), ↑(m i) ∣ (Polynomial.eval n (P.R i)).natAbs) : primeReject m P.discriminant.primeFactors ∈ weightUpTo P.exponent P.discriminant N ∧ primeSelect m P.discriminant.primeFactors ∈ smallBadParts P.exponent P.badDiscriminant (primeReject m P.discriminant.primeFactors) N

An actual polynomial divisor splits into an admissible good part and a bounded bad part.

theorem NairTenenbaum.PolynomialSystem.smallDivisorSiftedSum_le_split {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (N : ℕ+) (a b : ℤ) (z : ℝ) : P.smallDivisorSiftedSum F N a b z ≤ ∑ v ∈ weightUpTo P.exponent P.discriminant N, ∑ u ∈ smallBadParts P.exponent P.badDiscriminant v N, pullback P.exponent F (u * v) * ↑(P.badPrimeSiftedCount u v a b z)

theorem NairTenenbaum.exists_smallDivisorSiftedSum_bound {g : ℕ} (hg : 0 < g) {η δ : ℝ} (hη : 0 < η) (hδ : 0 < δ) : ∃ (K : ℝ) (L : ℝ), 1 ≤ K ∧ 1 ≤ L ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (A B ε : ℝ) (F : ArithmeticMap k), Admissible A B ε F → 0 ≤ A → 1 ≤ B → 0 < ε → ↑g ^ 2 * ε ≤ 1 / 8 → ∀ (N : ℕ+) (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → L * ↑↑N * z ^ (4 * ↑g * (1 + η) + δ) ≤ ↑b - ↑a → P.smallDivisorSiftedSum F N a b z ≤ K * smallDivisorSieveCost B ε g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total z * ∑ n ∈ Finset.Icc 1 N, P.weight F n

The corrected small-divisor sieve estimate in the original, unsplit tuple variables. A single level condition on N controls every tuple in the sum.