One coprimality sieve on a unit residue-class interval

Finite Mobius inversion costs only the divisors of the specified sieve integer. No coprimality between that integer and either modulus is assumed: divisors meeting the phase modulus vanish intrinsically, and divisors meeting the progression modulus are excluded by the unit residue. The surviving divisor sections are CRT progressions of step e * v.

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

Equations

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

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

Equations

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalDivisorInterval_eq_zero_of_not_coprime_modulus (q : ℕ) [NeZero q] (d : ℤ) (b v e L U : ℕ) (heq : ¬e.Coprime q) : reciprocalDivisorInterval q d b v e L U = 0

A divisor sharing the phase modulus forces every term to be a nonunit.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalDivisorInterval_eq_zero_of_not_coprime_step (q : ℕ) [NeZero q] (d : ℤ) (b v e L U : ℕ) (hbv : b.Coprime v) (hev : ¬e.Coprime v) : reciprocalDivisorInterval q d b v e L U = 0

A divisor sharing the step cannot divide an integer in a unit residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalDivisorInterval_eq_crt (q : ℕ) [NeZero q] (d : ℤ) (b v e L U : ℕ) (hev : e.Coprime v) : reciprocalDivisorInterval q d b v e L U = reciprocalResidueInterval q d (↑(Nat.chineseRemainder hev 0 b)) (e * v) L U

CRT gives one residue class modulo e*v, not an arbitrary filtered AP.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sievedReciprocalInterval_eq_moebius (q : ℕ) [NeZero q] (d : ℤ) (b v A L U : ℕ) (hA : A ≠ 0) : sievedReciprocalInterval q d b v A L U = ∑ e ∈ A.divisors, ↑(ArithmeticFunction.moebius e) * reciprocalDivisorInterval q d b v e L U

The finite Mobius expansion holds for the actual complex-valued phase.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sievedReciprocalInterval_eq_moebius_unit_divisors (q : ℕ) [NeZero q] (d : ℤ) (b v A L U : ℕ) (hA : A ≠ 0) (hbv : b.Coprime v) : sievedReciprocalInterval q d b v A L U = ∑ e ∈ A.divisors with e.Coprime q ∧ e.Coprime v, ↑(ArithmeticFunction.moebius e) * reciprocalDivisorInterval q d b v e L U

Divisors meeting either modulus can be deleted before estimating.

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

Each surviving divisor keeps the stronger interval length divided by e*v.

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

Cancellation on one genuine sieved residue interval.

The constant depends only on ε. In particular, A need not be coprime to q or v. The divisor cost is only A.divisors.card; the original interval span is divided by v*q, with no loss of the progression saving.