Theorem 1: short sums of admissible arithmetic functions #
The four majorants give a coefficient-independent height threshold and a bound constant depending only on the fixed parameters and the restricted discriminant. The bad-prime corrections retain all valuations throughout the proof.
theorem
NairTenenbaum.exists_shortSum_mainTerm_bound
{g : ℕ}
(hg : 0 < g)
{A B ε δ : ℝ}
(hA : 1 ≤ A)
(hB : 1 ≤ B)
(hε : 0 < ε)
(hsmall : ↑g ^ 2 * ε ≤ 1 / 8)
(hδ : 0 < δ)
(hδ₁ : δ ≤ 1)
:
∃ (c₀ : ℝ),
0 < c₀ ∧ ∃ (C : ℕ → ℝ),
(∀ (D : ℕ), 0 < C D) ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r),
P.total.natDegree = g →
∀ (F : ArithmeticMap k),
Admissible A B (ε * δ / 3) F →
∀ (x y : ℝ),
c₀ * ↑(polynomialHeight P.total) ^ δ < x →
x ^ (4 * ↑g ^ 2 * ε) ≤ y → y ≤ x → shortSum P.Q F x y ≤ C P.badDiscriminant * mainTerm P F x y
The short-sum estimate, with constants uniform also in the number of polynomials and irreducible factors at fixed total degree.
Theorem 1, equation (18), with the quantifier order recorded in Targets.
This is a proof of the original target proposition, not an additional hypothesis.