Arithmetic progressions as integer intervals after affine substitution

noncomputable def NairTenenbaum.progressionSum {k : ℕ} (Q : Fin k → Polynomial ℤ) (F : ArithmeticMap k) (q a : ℕ) (x y : ℝ) : ℝ

The short sum restricted to the residue class a modulo q.

Equations

• NairTenenbaum.progressionSum Q F q a x y = ∑ n ∈ NairTenenbaum.shortInterval x y with n ≡ a [MOD q], NairTenenbaum.extendArithmeticMap F fun (j : Fin k) => (Polynomial.eval (↑n) (Q j)).natAbs

noncomputable def NairTenenbaum.progressionMainTerm {k r : ℕ} (P : PolynomialSystem k r) (F : ArithmeticMap k) (q : ℕ) (x y : ℝ) : ℝ

The main term in Corollary 1.

Equations

• NairTenenbaum.progressionMainTerm P F q x y = y / ↑q * NairTenenbaum.progressionSieveProduct P.total q x * ∑ N ∈ NairTenenbaum.positiveUpTo x with q.Coprime ↑N, P.weight F N

theorem NairTenenbaum.PolynomialSystem.affine_mainTerm {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) (F : ArithmeticMap k) (x y : ℝ) : mainTerm (P.affine q a hq hqa) F x (y / ↑q) = progressionMainTerm P F q x y

theorem NairTenenbaum.mem_affine_interval_iff {q : ℕ} (hq : 0 < q) (a : ℤ) (x y : ℝ) (t : ℤ) : t ∈ Finset.Ioc ⌊(x - ↑a) / ↑q⌋ ⌊(x + y - ↑a) / ↑q⌋ ↔ x < ↑q * ↑t + ↑a ∧ ↑q * ↑t + ↑a ≤ x + y

Membership in the transformed interval is exactly membership of the integer affine value in the original real interval.

theorem NairTenenbaum.affine_interval_endpoint_bounds {q : ℕ} (hq : 0 < q) (a : ℤ) {x y : ℝ} (hy : 0 ≤ y) (hyq : 1 ≤ y / ↑q) : ⌊(x - ↑a) / ↑q⌋ ≤ ⌊(x + y - ↑a) / ↑q⌋ ∧ y / ↑q - 1 ≤ ↑⌊(x + y - ↑a) / ↑q⌋ - ↑⌊(x - ↑a) / ↑q⌋ ∧ ↑⌊(x + y - ↑a) / ↑q⌋ - ↑⌊(x - ↑a) / ↑q⌋ ≤ 2 * (y / ↑q)

Integer rounding costs less than one unit of transformed length.

theorem NairTenenbaum.PolynomialSystem.progressionSum_le_affine_integerSum {k r : ℕ} (P : PolynomialSystem k r) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (q a : ℕ) (hq : 0 < q) (hqa : q.Coprime (Polynomial.eval (↑a) P.total).natAbs) {x y : ℝ} (hxy : 0 ≤ x + y) : progressionSum P.Q F q a x y ≤ (P.affine q ↑a ⋯ hqa).integerSum F ⌊(x - ↑a) / ↑q⌋ ⌊(x + y - ↑a) / ↑q⌋

Reindexing by (n-a)/q bounds the progression sum by the integer sum of the substituted family. Negative transformed indices are allowed.