Reciprocal sums on genuine residue-class intervals

The interval is a natural-number interval, not an arbitrary mask on a progression. Choosing its first admissible point retains multiplicities and gives a parameter interval whose length is bounded by the original span divided by the step.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalResidueInterval (q : ℕ) [NeZero q] (d : ℤ) (b v L U : ℕ) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalResidueInterval q d b v L U = ∑ k ∈ Finset.Icc L U, if k % v = b % v then MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalPhase q d ↑k else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalProgression_nat_Icc (q : ℕ) [NeZero q] (d : ℤ) (b v N : ℕ) : ∑ t ∈ Finset.Icc 0 N, reciprocalPhase q d ↑(b + v * t) = reciprocalProgression q d (↑b) v (-1) ↑N

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalResidueInterval_eq_progression (q : ℕ) [NeZero q] (d : ℤ) (b v L U : ℕ) (hv : 0 < v) (hne : {k ∈ Finset.Icc L U | k % v = b % v}.Nonempty) : ∃ (c : ℕ) (N : ℕ), L ≤ c ∧ c ≤ U ∧ c % v = b % v ∧ N * v ≤ U - L ∧ reciprocalResidueInterval q d b v L U = reciprocalProgression q d (↑c) v (-1) ↑N

Nonempty residue sections are actual progressions, with a length certificate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalResidueInterval_fouvry {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℕ) (x : NeZero q) (d : ℤ) (b v L U : ℕ), 0 < v → v.Coprime q → ‖reciprocalResidueInterval q d b v L U‖ ≤ C * (1 + ↑(U - L + 1) / (↑v * ↑q)) * √↑(q.gcd d.natAbs) * ↑q ^ (1 / 2 + ε)

A uniform interval bound with the original span divided by the step. The constant absorbs at most a factor two from the first point of the AP.