A single large-prefix band bounded by the main term

theorem NairTenenbaum.exists_primeBandSiftedSum_mainTerm_bound {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ) (x₀ : ℝ), 0 < K ∧ 1 ≤ x₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (A B σ κ c : ℝ) (F : ArithmeticMap k), Admissible A B σ F → 1 ≤ A → 1 ≤ B → 0 < σ → 0 ≤ κ → ↑g ^ 2 * σ ≤ 1 / 8 → c * Real.log A + 4 * ↑g * Real.log 4 + 1 ≤ κ * (3 * ↑g ^ 2 * ε / 2) / 2 → ∀ (x y α : ℝ) (N : ℕ+) (a b : ℤ), x₀ ≤ x → 1 < x → 1 ≤ Real.log x → 0 < α → 2 * α ≤ 1 → α ≤ ↑g * ε / 16 → 2 ≤ x ^ α → 2 * ↑g ≤ x ^ α → 16 ≤ Real.log (x ^ α) → 8 * ↑g ^ 2 * κ ≤ Real.log (x ^ (2 * α)) → ↑↑N ≤ x ^ (3 * ↑g ^ 2 * ε) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y / 2 ≤ ↑b - ↑a → ↑b - ↑a ≤ 2 * y → A ^ (c / α) * P.smoothTailSiftedSum F N (Finset.Icc 0 ⌊x ^ (2 * α)⌋₊) (x ^ (3 * ↑g ^ 2 * ε / 2)) a b (x ^ α) ≤ K * smoothTailSieveCost A B κ g P.badDiscriminant * Real.exp (-1 / α) * mainTerm P F x y

Uniform sieve and moment estimate for one logarithmic prime band. The moment strength pays the rough-remainder and Euler-product costs. Neither the constant nor the lower threshold depends on the band's exponent α.