Theorem 3: short sums at prime arguments #
The proof keeps the original polynomial family in the value decomposition
and sieves its product with X only at admissible primes. The constants have
the same degree, growth-parameter, and restricted-discriminant uniformity as
in Theorem 1; the constant-term correction remains explicit in the main term.
theorem
NairTenenbaum.exists_primeShortSum_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 →
Polynomial.eval 0 P.total ≠ 0 →
∀ (F : ArithmeticMap k),
Admissible A B (ε * δ / 3) F →
∀ (x y : ℝ),
c₀ * ↑(polynomialHeight P.total) ^ δ < x →
x ^ (4 * ↑g ^ 2 * ε) ≤ y →
y ≤ x → primeShortSum P.Q F x y ≤ C P.badDiscriminant * primeMainTerm P F x y
Theorem 3, with a coefficient-independent height threshold and the restricted-discriminant dependence displayed in the order of quantifiers.
Equations
- One or more equations did not get rendered due to their size.