Reducing Hooley short sums to primitive affine restrictions

theorem NairTenenbaum.hooleyDelta_affine_eval_le (Q : Polynomial ℤ) (M a n : ℤ) : hooleyDelta (Polynomial.eval (M * n + a) Q).natAbs ≤ (affineRestriction Q M a).content.natAbs.divisors.card * hooleyDelta (Polynomial.eval n (affineRestriction Q M a).primPart).natAbs

theorem NairTenenbaum.hooley_affine_eval_rpow_le (Q : Polynomial ℤ) (M a n : ℤ) {t : ℝ} (ht : 0 ≤ t) : ↑(hooleyDelta (Polynomial.eval (M * n + a) Q).natAbs) ^ t ≤ ↑(affineRestriction Q M a).content.natAbs.divisors.card ^ t * ↑(hooleyDelta (Polynomial.eval n (affineRestriction Q M a).primPart).natAbs) ^ t

theorem NairTenenbaum.quotient_mem_affine_shortInterval {M a n : ℕ} (hM : 0 < M) (ha : a < M) {x y : ℝ} (hx : ↑M ≤ x) (hy : 0 ≤ y) (hn : n ∈ shortInterval x y) (hr : n % M = a) : n / M ∈ shortInterval ((x - ↑a) / ↑M) (y / ↑M)

theorem NairTenenbaum.hooleyPolynomialSum_residue_le (Q : Polynomial ℤ) {M a : ℕ} (hM : 0 < M) (ha : a < M) {t x y : ℝ} (ht : 0 ≤ t) (hx : ↑M ≤ x) (hy : 0 ≤ y) : ∑ n ∈ shortInterval x y with n % M = a, ↑(hooleyDelta (Polynomial.eval (↑n) Q).natAbs) ^ t ≤ ↑(affineRestriction Q ↑M ↑a).content.natAbs.divisors.card ^ t * hooleyPolynomialSum (affineRestriction Q ↑M ↑a).primPart t ((x - ↑a) / ↑M) (y / ↑M)

theorem NairTenenbaum.hooleyPolynomialSum_le_affine_primitive_sums (Q : Polynomial ℤ) {M : ℕ} (hM : 0 < M) {t x y : ℝ} (ht : 0 ≤ t) (hx : ↑M ≤ x) (hy : 0 ≤ y) : hooleyPolynomialSum Q t x y ≤ ∑ a ∈ Finset.range M, ↑(affineRestriction Q ↑M ↑a).content.natAbs.divisors.card ^ t * hooleyPolynomialSum (affineRestriction Q ↑M ↑a).primPart t ((x - ↑a) / ↑M) (y / ↑M)