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.smoothTailSieveCost (A B κ : ℝ) (g D : ℕ) : ℝ

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

Equations

• NairTenenbaum.smoothTailSieveCost A B κ g D = NairTenenbaum.totientTwist g D * NairTenenbaum.splitSmoothTailBound A B κ g D

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

theorem NairTenenbaum.exists_smoothTailSiftedSum_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 → ∀ (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 + η) + δ) ≤ ↑b - ↑a → P.smoothTailSiftedSum F N (Finset.Icc 0 ⌊w⌋₊) X a b z ≤ K * smoothTailSieveCost 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

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.