A uniform sieve level for large prefixes

Reducing the prime cutoff to x^(g*ε/16) leaves room to sieve all prefixes of weighted mass at most x^(3*g²*ε). Every smaller prime cutoff shares the same lower threshold on x.

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

theorem NairTenenbaum.exists_largePrefix_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 / 16) + 1 / 4) ≤ y / 2

A single height threshold supplies the conditional sieve level throughout the large-prefix prime bands. The logarithmic lower bound on an individual band cutoff is separate from this upper-cutoff estimate.

theorem NairTenenbaum.exists_largePrefixSiftedSum_at_scales {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ) (x₀ : ℝ), 1 ≤ K ∧ 1 ≤ x₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (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.smallDivisorSiftedSum F N a b (x ^ (↑g * ε / 16)) ≤ K * smallDivisorSieveCost B σ g P.badDiscriminant * (↑b - ↑a) * sieveProduct P.total (x ^ (↑g * ε / 16)) * ∑ n ∈ Finset.Icc 1 N, P.weight F n

The original sifted divisor sum at the large-prefix scale.