Selected smooth prefixes with a lower mass cutoff

theorem NairTenenbaum.PolynomialSystem.sum_selectedSmoothTailDivisors_le {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (N : ℕ+) (s : Finset ℕ) (X : ℝ) (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)) (hsmooth : ∀ t ∈ T, ∀ (i : Fin r), ↑(m t i) ∈ Nat.factoredNumbers s) (hlarge : ∀ t ∈ T, X < ↑(weightedMass P.exponent (m t))) (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.smoothTailSiftedSum F N s X a b z

Grouping selected divisors preserves both smoothness and the lower mass cutoff. Distinct integers can have the same selected tuple.

theorem NairTenenbaum.PolynomialSystem.sum_roughSmoothTailPrefix_le {k r : ℕ} (P : PolynomialSystem k r) {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hA : 1 ≤ A) (hB : 0 ≤ B) (N : ℕ+) (s : Finset ℕ) (X : ℝ) (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) (hsmooth : ∀ t ∈ T, ∀ (i : Fin r), ↑(primeSelect (n t) (Finset.range (q t)) i) ∈ Nat.factoredNumbers s) (hlarge : ∀ t ∈ T, X < ↑(weightedMass P.exponent (primeSelect (n t) (Finset.range (q t))))) (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.smoothTailSiftedSum F N s X a b (x ^ α)

Rough remainders can be removed while retaining the smooth mass tail of the selected prefix. The sifting cutoff is x^α; its relation to the smoothness support is unrestricted.