Reindexing the original smooth mass tail under the sieve restriction

noncomputable def NairTenenbaum.smoothTailDivisorTuples {k r : ℕ} (γ : Fin k → Fin r → ℕ) (N : ℕ+) (s : Finset ℕ) (X : ℝ) : Finset (Tuple r)

Small divisor tuples supported on the chosen primes with mass above the tail cutoff.

Equations

• NairTenenbaum.smoothTailDivisorTuples γ N s X = {m ∈ NairTenenbaum.smallDivisorTuples γ N | (∀ (i : Fin r), ↑(m i) ∈ Nat.factoredNumbers s) ∧ X < ↑(NairTenenbaum.weightedMass γ m)}

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

Sifted divisor sum restricted by smoothness and a lower weighted-mass cutoff.

Equations

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

theorem NairTenenbaum.PolynomialSystem.smoothTailDivisor_split_mem {k r : ℕ} (P : PolynomialSystem k r) (N : ℕ+) (s : Finset ℕ) (X : ℝ) (m : Tuple r) (hm : m ∈ smoothTailDivisorTuples P.exponent N s X) (n : ℤ) (hdiv : ∀ (i : Fin r), ↑(m i) ∣ (Polynomial.eval n (P.R i)).natAbs) : primeReject m P.discriminant.primeFactors ∈ smoothWeightUpTo P.exponent P.discriminant s N ∧ primeSelect m P.discriminant.primeFactors ∈ {u ∈ smallBadParts P.exponent P.badDiscriminant (primeReject m P.discriminant.primeFactors) N | X < ↑(weightedMass P.exponent (u * primeReject m P.discriminant.primeFactors))}

Whole-prime-power splitting preserves the good-part smoothness and combined mass tail.

theorem NairTenenbaum.PolynomialSystem.smoothTailSiftedSum_le_split {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (N : ℕ+) (s : Finset ℕ) (X : ℝ) (a b : ℤ) (z : ℝ) : P.smoothTailSiftedSum F N s X a b z ≤ ∑ v ∈ smoothWeightUpTo P.exponent P.discriminant s N, ∑ u ∈ smallBadParts P.exponent P.badDiscriminant v N with X < ↑(weightedMass P.exponent (u * v)), pullback P.exponent F (u * v) * ↑(P.badPrimeSiftedCount u v a b z)

The combined mass tail survives full bad-prime splitting unchanged. Only positive-count tuples require a witness for the discriminant conditions.