A uniform short-sum bound from polynomial-value growth

This form keeps the analytic scale independent of the location of the integer interval. All constants are chosen before the polynomial system; only the upper-bound constant depends on its restricted discriminant.

theorem NairTenenbaum.exists_integerSum_mainTerm_bound {g : ℕ} (hg : 0 < g) {A B ε σ c : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) (hσ : 0 < σ) (hσsmall : ↑g ^ 2 * σ ≤ 1 / 8) (hc : 0 ≤ c) (hmargin : c * σ ≤ 17 * ↑g * ε / 24) : ∃ (x₀ : ℝ), 1 < x₀ ∧ ∃ (C : ℕ → ℝ), (∀ (D : ℕ), 0 < C D) ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (F : ArithmeticMap k), Admissible A B σ F → ∀ (x y : ℝ) (a b : ℤ), x₀ ≤ x → 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) → P.integerSum F a b ≤ C P.badDiscriminant * mainTerm P F x y

Short sums over arbitrary integer intervals, assuming a bound on the actual polynomial values and a positive margin between arithmetic growth and the exceptional-set saving.

theorem NairTenenbaum.PolynomialSystem.integerSum_le_of_value_bound {k r : ℕ} (P : PolynomialSystem k r) {A B σ c x y : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hB : 0 ≤ B) (hσ : 0 ≤ σ) (hx : 0 ≤ x) {a b : ℤ} (hab : a ≤ b) (hlen : ↑b - ↑a ≤ 2 * y) (hvalue : ∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : P.integerSum F a b ≤ 2 * B * y * x ^ (c * σ) * F 1

The elementary bound used on a bounded range of the analytic scale.

theorem NairTenenbaum.exists_integerSum_mainTerm_bound_all_scales {g : ℕ} (hg : 0 < g) {A B ε σ c : ℝ} (hA : 1 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) (hσ : 0 < σ) (hσsmall : ↑g ^ 2 * σ ≤ 1 / 8) (hc : 0 ≤ c) (hmargin : c * σ ≤ 17 * ↑g * ε / 24) : ∃ (C : ℕ → ℝ), (∀ (D : ℕ), 0 < C D) ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (F : ArithmeticMap k), Admissible A B σ F → ∀ (x y : ℝ) (a b : ℤ), 2 ≤ x → x ^ (4 * ↑g ^ 2 * ε) ≤ y → a ≤ b → y - 1 ≤ ↑b - ↑a → ↑b - ↑a ≤ 2 * y → (∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) → P.integerSum F a b ≤ C P.badDiscriminant * mainTerm P F x y

Enlarging the upper-bound constant handles the bounded range of x, so the value-bound estimate is valid for every x ≥ 2. In applications this keeps the coefficient-height threshold independent of an interval parameter.