The conditional sieve on a smooth mass tail

The smoothness cutoff and the sieve cutoff are separate. This permits grouping prefixes into bands whose upper and lower prime cutoffs differ.

noncomputable def NairTenenbaum.primeArgumentTailSieveCost (A B κ : ℝ) (g D : ℕ) : ℝ

The discriminant-dependent cost of the prime-argument smooth-tail sieve.

Equations

• NairTenenbaum.primeArgumentTailSieveCost A B κ g D = NairTenenbaum.totientTwist (g + 1) D * NairTenenbaum.primeArgumentSplitTailBound A B κ g D

theorem NairTenenbaum.primeArgumentTailSieveCost_pos {A B κ : ℝ} (hB : 0 < B) {g D : ℕ} (hg : 0 < g) (hD : 0 < D) : 0 < primeArgumentTailSieveCost A B κ g D

theorem NairTenenbaum.exists_primeSmoothTailSiftedSum_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 < ε → 0 ≤ κ → ↑g ^ 2 * ε ≤ 1 / 8 → ∀ (w X : ℝ), 2 ≤ w → 8 * ↑g ^ 2 * κ ≤ Real.log w → 0 < X → ∀ (N : ℕ+) (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → L * ↑↑N * z ^ (4 * (↑g + 1) * (1 + η) + δ) ≤ ↑b - ↑a → P.primeSmoothTailSiftedSum F g N (Finset.Icc 0 ⌊w⌋₊) X a b z ≤ (K * primeArgumentTailSieveCost A B κ g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total z * Real.exp (-κ * Real.log X / Real.log w) * ∑ n ∈ positiveUpTo w, P.weight F n) * primeArgumentFactor P.total z

The sieve bound for an original smooth divisor tail, with uniform constants and all bad-prime moments accounted for. The cutoff for smoothness is w, and the cutoff for sifting is z.