Summing the large-prefix logarithmic bands

theorem NairTenenbaum.exists_primeBandSum_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 u : ℝ) (N : ℕ+) (a b : ℤ) (J : Finset ℕ), x₀ ≤ x → 1 < x → 1 ≤ Real.log x → 0 < u → u ≤ 1 → u ≤ ↑g * ε / 16 → (∀ j ∈ J, 2 ≤ x ^ (u / 2 ^ (j + 1)) ∧ 2 * ↑g ≤ x ^ (u / 2 ^ (j + 1)) ∧ 16 ≤ Real.log (x ^ (u / 2 ^ (j + 1))) ∧ 8 * ↑g ^ 2 * κ ≤ Real.log (x ^ (2 * (u / 2 ^ (j + 1))))) → ↑↑N ≤ x ^ (3 * ↑g ^ 2 * ε) → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y / 2 ≤ ↑b - ↑a → ↑b - ↑a ≤ 2 * y → (∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) → ∑ j ∈ J, P.smoothTailPrefixContribution F N (Finset.Icc 0 ⌊x ^ (2 * (u / 2 ^ (j + 1)))⌋₊) (x ^ (3 * ↑g ^ 2 * ε / 2)) a b (x ^ (u / 2 ^ (j + 1))) ≤ K * smoothTailSieveCost A B κ g P.badDiscriminant * mainTerm P F x y

The sum of the original weighted contributions over any finite collection of eligible bands is bounded uniformly in the number of bands.