From selected polynomial divisors to the sifted tuple sum

theorem NairTenenbaum.PolynomialSystem.sum_selectedDivisors_le {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (N : ℕ+) (a b : ℤ) (z : ℝ) (T : Finset ℤ) (m : ℤ → Tuple r) (hT : T ⊆ Finset.Ioc a b) (hm : ∀ t ∈ T, weightedMass P.exponent (m t) ≤ ↑N) (hdiv : ∀ t ∈ T, ∀ (i : Fin r), ↑↑(m t i) ∣ Polynomial.eval t (P.R i)) (hsift : ∀ t ∈ T, (sieveModulus P.total (mass (m t)) z).Coprime (Polynomial.eval t P.total).natAbs) : ∑ t ∈ T, pullback P.exponent F (m t) ≤ P.smallDivisorSiftedSum F N a b z

Grouping a selected divisor for each integer by its tuple gives the sifted small-divisor majorant. Distinct integers can have the same selected tuple.

theorem NairTenenbaum.PolynomialSystem.sum_roughPrefix_le {k r : ℕ} (P : PolynomialSystem k r) {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hA : 1 ≤ A) (hB : 0 ≤ B) (N : ℕ+) (a b : ℤ) (T : Finset ℤ) (n : ℤ → Tuple r) (q : ℤ → ℕ) (hT : T ⊆ Finset.Ioc a b) (hn : ∀ t ∈ T, ∀ (i : Fin r), ↑(n t i) = (Polynomial.eval t (P.R i)).natAbs) {x α c : ℝ} (hx : 1 < x) (hα : 0 < α) (hq : ∀ t ∈ T, x ^ α < ↑(q t)) (hsmall : ∀ t ∈ T, weightedMass P.exponent (primeSelect (n t) (Finset.range (q t))) ≤ ↑N) (hvalue : ∀ t ∈ T, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : (∑ t ∈ T, extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval t (P.Q j)).natAbs) ≤ A ^ (c / α) * P.smallDivisorSiftedSum F N a b (x ^ α)

Equation (31), with explicit growth constant and a proven sieve condition. The finite set can be any part of the interval whose selected prefixes are small and whose next-prime cutoffs exceed x^α.