Summing the prime-argument sieve over the small good tuples

noncomputable def NairTenenbaum.primeArgumentSmallSieveCost (B ε : ℝ) (g D : ℕ) : ℝ

The discriminant-dependent cost of the small-divisor sieve at prime arguments.

Equations

• NairTenenbaum.primeArgumentSmallSieveCost B ε g D = NairTenenbaum.primeArgumentBadSieveCost B g D * NairTenenbaum.totientExponentComparisonBound B ε g (g + 1) D

theorem NairTenenbaum.exists_primeArgument_small_sieve_sum_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 < ε → ↑g ^ 2 * ε ≤ 1 / 8 → ∀ (N : ℕ+) (S : Tuple r → Finset (Tuple r)), (∀ v ∈ weightUpTo P.exponent P.discriminant N, ∀ u ∈ S v, ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors) → ∀ (a b : ℤ) (z : ℝ), a ≤ b → 2 ≤ z → 16 ≤ Real.log z → (∀ v ∈ weightUpTo P.exponent P.discriminant N, ∀ u ∈ S v, L * ↑(tupleLCM u) * ↑(mass v) * z ^ (4 * (↑g + 1) * (1 + η) + δ) ≤ ↑b - ↑a) → ∑ v ∈ weightUpTo P.exponent P.discriminant N, ∑ u ∈ S v, pullback P.exponent F (u * v) * ↑(P.primeArgumentBadSiftedCount g u v a b z) ≤ (K * primeArgumentSmallSieveCost B ε g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total z * ∑ n ∈ Finset.Icc 1 N, P.weight F n) * primeArgumentFactor P.total z

A finite family of bad-prime parts over all small dagger tuples is bounded by the original weight sum. The sieve level is required only for the parts actually present in each finite family.