A logarithmic prime band with the additional prime-argument saving

theorem NairTenenbaum.primeArgument_band_decay {A c κ τ α x : ℝ} {g : ℕ} (hA : 0 < A) (hα : 0 < α) (hx : 1 < x) (hκ : c * Real.log A + 4 * ↑g * Real.log 4 + 2 ≤ κ * τ / 2) : A ^ (c / α) * Real.exp (4 * ↑g * Real.log 4 / α) * Real.exp (-κ * Real.log (x ^ τ) / Real.log (x ^ (2 * α))) / α ≤ Real.exp (-1 / α)

theorem NairTenenbaum.exists_primeArgumentBandSiftedSum_mainTerm_bound {g : ℕ} (hg : 0 < g) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ) (x₀ : ℝ), 0 < K ∧ 1 ≤ x₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → Polynomial.eval 0 P.total ≠ 0 → ∀ (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 + 2 ≤ κ * (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.primeSmoothTailSiftedSum F g N (Finset.Icc 0 ⌊x ^ (2 * α)⌋₊) (x ^ (3 * ↑g ^ 2 * ε / 2)) a b (x ^ α) ≤ K * primeArgumentTailSieveCost A B κ g P.badDiscriminant * Real.exp (-1 / α) * primeMainTerm 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 α.