Sieve levels for prime arguments with the original degree and growth exponent

theorem NairTenenbaum.primeArgument_scale_exponent {g : ℕ} (hg : 0 < g) (ε : ℝ) (hε : 0 ≤ ε) : 3 * ↑g ^ 2 * ε + ↑g * ε / 16 * (4 * (↑g + 1) * (1 + 1 / 16) + 1 / 4) + ↑g ^ 2 * ε / 4 ≤ 4 * ↑g ^ 2 * ε

The smaller prime cutoff accommodates the enlarged sieve dimension, even for prefix masses up to x^(3g²ε).

theorem NairTenenbaum.exists_primeArgument_sieve_scales {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) {L : ℝ} (hL : 1 ≤ L) : ∃ (x₀ : ℝ), 1 ≤ x₀ ∧ ∀ (x : ℝ), x₀ ≤ x → 2 ≤ x ^ (↑g * ε / 16) ∧ 16 ≤ Real.log (x ^ (↑g * ε / 16)) ∧ ∀ (N y : ℝ), 0 ≤ N → N ≤ x ^ (3 * ↑g ^ 2 * ε) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → L * N * (x ^ (↑g * ε / 16)) ^ (4 * (↑g + 1) * (1 + 1 / 16) + 1 / 4) ≤ y / 2

One uniform threshold makes the chosen cutoffs satisfy the logarithmic and size conditions of the conditional sieve, including a factor two for passing to integer endpoints.

theorem NairTenenbaum.exists_primeArgument_variable_sieve_scales {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) {L : ℝ} (hL : 1 ≤ L) : ∃ (x₀ : ℝ), 1 ≤ x₀ ∧ ∀ (x : ℝ), x₀ ≤ x → ∀ (N y z : ℝ), 0 ≤ N → N ≤ x ^ (3 * ↑g ^ 2 * ε) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → 0 ≤ z → z ≤ x ^ (↑g * ε / 16) → L * N * z ^ (4 * (↑g + 1) * (1 + 1 / 16) + 1 / 4) ≤ y / 2

The same threshold works throughout all smaller logarithmic bands.

theorem NairTenenbaum.exists_primeSmallDivisorSiftedSum_at_scales {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ) (x₀ : ℝ), 1 ≤ K ∧ 1 ≤ x₀ ∧ ∀ (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 → ∀ (x y : ℝ) (N : ℕ+) (a b : ℤ), x₀ ≤ x → ↑↑N ≤ x ^ (3 * ↑g ^ 2 * ε) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y / 2 ≤ ↑b - ↑a → P.primeSmallDivisorSiftedSum F g N a b (x ^ (↑g * ε / 16)) ≤ (K * primeArgumentSmallSieveCost B σ g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total (x ^ (↑g * ε / 16)) * ∑ n ∈ Finset.Icc 1 N, P.weight F n) * primeArgumentFactor P.total (x ^ (↑g * ε / 16))

The divisor sum at the reduced sieve cutoff, with constants chosen before all polynomial coefficients and the admissible arithmetic function.