The prime-argument sieve in the original divisor tuple variables

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

theorem NairTenenbaum.PolynomialSystem.primeSmallDivisorSiftedSum_le_split {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (g : ℕ) (N : ℕ+) (a b : ℤ) (z : ℝ) : P.primeSmallDivisorSiftedSum F g 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.primeArgumentBadSiftedCount g u v a b z)

theorem NairTenenbaum.exists_primeSmallDivisorSiftedSum_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 → Polynomial.eval 0 P.total ≠ 0 → ∀ (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) * (1 + η) + δ) ≤ ↑b - ↑a → P.primeSmallDivisorSiftedSum F g N a b z ≤ (K * primeArgumentSmallSieveCost B ε g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total z * ∑ n ∈ Finset.Icc 1 N, P.weight F n) * primeArgumentFactor P.total z

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