Reindexing the smooth prefix tail for prime arguments

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

The smooth mass-tail divisor sum sifted for prime arguments.

Equations

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

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