Summing logarithmic prefix bands at prime arguments

The moment strength pays the extra reciprocal band exponent. The resulting geometric majorant and lower smoothness cutoff are uniform in the polynomial coefficients and in the number of bands.

theorem NairTenenbaum.exists_primeArgumentBandSum_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 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.primeSmoothTailPrefixContribution F N (Finset.Icc 0 ⌊x ^ (2 * (u / 2 ^ (j + 1)))⌋₊) (x ^ (3 * ↑g ^ 2 * ε / 2)) a b (x ^ (u / 2 ^ (j + 1))) ≤ K * primeArgumentTailSieveCost A B κ g P.badDiscriminant * primeMainTerm 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.

theorem NairTenenbaum.exists_primeArgumentBand_moment {g : ℕ} (hg : 0 < g) {ε A c : ℝ} (hε : 0 < ε) (hA : 1 ≤ A) (hc : 0 ≤ c) : ∃ (κ : ℝ), 0 < κ ∧ c * Real.log A + 4 * ↑g * Real.log 4 + 2 ≤ κ * (3 * ↑g ^ 2 * ε / 2) / 2

A moment strength with strictly positive decay margin always exists for the nonnegative polynomial-value exponent used in the main proof.

theorem NairTenenbaum.exists_primeArgumentBands_mainTerm_bound {g : ℕ} (hg : 0 < g) {ε A c : ℝ} (hε : 0 < ε) (hA : 1 ≤ A) (hc : 0 ≤ c) : ∃ (K : ℝ) (x₀ : ℝ) (κ : ℝ) (w₀ : ℝ), 0 < K ∧ 1 ≤ x₀ ∧ 0 < κ ∧ 1 < w₀ ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → Polynomial.eval 0 P.total ≠ 0 → ∀ (B σ : ℝ) (F : ArithmeticMap k), Admissible A B σ F → 1 ≤ B → 0 < σ → ↑g ^ 2 * σ ≤ 1 / 8 → ∀ (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, w₀ ≤ 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.primeSmoothTailPrefixContribution F N (Finset.Icc 0 ⌊x ^ (2 * (u / 2 ^ (j + 1)))⌋₊) (x ^ (3 * ↑g ^ 2 * ε / 2)) a b (x ^ (u / 2 ^ (j + 1))) ≤ K * primeArgumentTailSieveCost A B κ g P.badDiscriminant * primeMainTerm P F x y

All bands above a single fixed smoothness cutoff satisfy the summed main-term bound. The moment and cutoff are chosen before the polynomials.