Uniform bounds in arithmetic progressions

The affine family is estimated at the original scale x, using the original polynomial values. The bounded-scale estimate keeps the height threshold independent of the progression-length parameter β.

theorem NairTenenbaum.progression_length_lower {g q : ℕ} {ε β x y : ℝ} (hq : 0 < q) (hx : 0 < x) (hβ : 0 ≤ β) (hy : x ^ (4 * ↑g ^ 2 * ε) ≤ y) (hqty : ↑q ≤ y ^ (1 - β)) : x ^ (4 * ↑g ^ 2 * (ε * β)) ≤ y / ↑q

The modulus restriction leaves enough transformed interval length for the exponent εβ.

theorem NairTenenbaum.progression_growth_margin {g : ℕ} (hg : 0 < g) {ε β δ : ℝ} (hε : 0 ≤ ε) (hβ : 0 ≤ β) (hδ : 0 < δ) (hδ₁ : δ ≤ 1 / 2) : (↑g + 1 / (2 * δ) + 1) * (ε * β * δ / 6) ≤ ↑g * (ε * β) / 2

The explicit value exponent and arithmetic growth satisfy the uniform interval theorem's saving margin.

theorem NairTenenbaum.PolynomialSystem.affine_interval_value_bound {k r g : ℕ} (P : PolynomialSystem k r) (hdeg : P.total.natDegree = g) (q a : ℕ) (hq : 0 < q) (hqa : q.Coprime (Polynomial.eval (↑a) P.total).natAbs) {x y δ : ℝ} (hx : 1 ≤ x) (hyx : y ≤ x) (hδ : 0 < δ) (hheight : ↑(polynomialHeight P.total) ^ (2 * δ) ≤ x) (hlarge : (↑g + 1) * 2 ^ g ≤ x) (t : ℤ) : t ∈ Finset.Ioc ⌊(x - ↑a) / ↑q⌋ ⌊(x + y - ↑a) / ↑q⌋ → ↑(Polynomial.eval t (P.affine q ↑a ⋯ hqa).total).natAbs ≤ x ^ (↑g + 1 / (2 * δ) + 1)

Values in the transformed interval retain the original height bound.

theorem NairTenenbaum.exists_progressionSum_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 / 2) : ∃ (c₁ : ℝ), 0 < c₁ ∧ ∀ (β : ℝ), 0 < β → β < 1 → ∃ (C : ℕ → ℝ), (∀ (D : ℕ), 0 < C D) ∧ ∀ (k r : ℕ) (P : PolynomialSystem k r), P.total.natDegree = g → ∀ (F : ArithmeticMap k), Admissible A B (ε * β * δ / 6) F → ∀ (q a : ℕ), 0 < q → q.Coprime (Polynomial.eval (↑a) P.total).natAbs → ∀ (x y : ℝ), c₁ * ↑(polynomialHeight P.total) ^ (2 * δ) < x → x ^ (4 * ↑g ^ 2 * ε) ≤ y → y ≤ x → ↑q ≤ y ^ (1 - β) → progressionSum P.Q F q a x y ≤ C P.badDiscriminant * progressionMainTerm P F q x y

Corollary 1 with constants uniform also in the number of factors. The height threshold is chosen before β; the bound constant may depend on it.