Reciprocal cancellation on unit-step arithmetic progressions

The step is a unit modulo the modulus, not necessarily one as an integer. The integer parameter retains its multiplicity on intervals longer than the modulus. Only the inherent nonunit vanishing of reciprocalPhase is imposed.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalProgression (q : ℕ) [NeZero q] (d b : ℤ) (v : ℕ) (X Y : ℤ) : ℂ

The actual unweighted sum over the integer parameter X < t ≤ Y.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalProgression q d b v X Y = ∑ t ∈ Finset.Ioc X Y, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalPhase q d ↑(b + ↑v * t)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalPhase_unit_mul {q v : ℕ} [NeZero q] (hv : v.Coprime q) (d : ℤ) (z : ZMod q) : reciprocalPhase q d (↑v * z) = reciprocalPhase q (d * wPhaseInverse v q) z

Multiplying the argument by a unit twists only the frequency.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalProgression_eq_reciprocalInterval {q v : ℕ} [NeZero q] (hv : v.Coprime q) (d b X Y : ℤ) : reciprocalProgression q d b v X Y = reciprocalInterval q (d * wPhaseInverse v q) ↑(X + b * wPhaseInverse v q) ↑(Y + b * wPhaseInverse v q)

Exact reduction to a shifted integer interval. There is no reduction of the parameter modulo q, so repeated residues are counted correctly.

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

The same short-interval constant works uniformly in the start and step.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalProgression_add (q : ℕ) [NeZero q] (d b : ℤ) (v : ℕ) {X M Y : ℤ} (hXM : X ≤ M) (hMY : M ≤ Y) : reciprocalProgression q d b v X M + reciprocalProgression q d b v M Y = reciprocalProgression q d b v X Y

Exact adjacent-interval splitting, also for intervals longer than q.

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

Unconditional individual cancellation on an arbitrarily long AP. The constant is precisely a short-interval Fouvry constant; there is no additional constant loss. The length factor counts successive modulus-sized blocks without identifying repeated residues.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalProgression_nat {q : ℕ} [NeZero q] (d : ℤ) (b v X Y : ℕ) : ∑ t ∈ Finset.Ioc X Y, reciprocalPhase q d ↑(b + v * t) = reciprocalProgression q d (↑b) v ↑X ↑Y

Natural parameters use exactly the same integer AP, with no endpoint loss.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationProgression (D d₁ n n₂ n₂' r s s' : ℕ) (a h h' : ℤ) (b v X Y : ℕ) : ℂ

The actual paired IV.3 phase on a natural-parameter AP, with only its coprimality restriction. For positive step, every sampled natural is positive.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationProgression D d₁ n n₂ n₂' r s s' a h h' b v X Y = ∑ t ∈ Finset.Ioc X Y with (b + v * t).Coprime (n * r * s * s'), (fourier h) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalPhase D d₁ n n₂ (b + v * t) r s a) * star ((fourier h') (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalPhase D d₁ n n₂' (b + v * t) r s' a))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationProgression_eq_reciprocalProgression {D d₁ n n₂ n₂' r s s' : ℕ} (hn : 0 < n) (hr : 0 < r) (hs : 0 < s) (hs' : 0 < s') (hB : (D * n₂ * n₂').Coprime (n * r * s * s')) (a h h' : ℤ) (b v X Y : ℕ) : iv3CorrelationProgression D d₁ n n₂ n₂' r s s' a h h' b v X Y = reciprocalProgression (n * r * s * s') (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' * wPhaseInverse (D * n₂ * n₂') (n * r * s * s')) (↑b) v ↑X ↑Y

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationProgression_fouvry {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (D d₁ n n₂ n₂' r s s' : ℕ) (a h h' : ℤ) (b v X Y : ℕ), 0 < n → 0 < r → 0 < s → 0 < s' → (D * n₂ * n₂').Coprime (n * r * s * s') → v.Coprime (n * r * s * s') → X ≤ Y → ‖iv3CorrelationProgression D d₁ n n₂ n₂' r s s' a h h' b v X Y‖ ≤ C * (1 + (↑Y - ↑X) / ↑(n * r * s * s')) * √↑((n * r * s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs) * ↑(n * r * s * s') ^ (1 / 2 + ε)

Paired IV.3 cancellation after freezing a residue class, uniformly in its start and unit step and in the signed residue/frequencies. No extra mask or arbitrary coefficients are allowed. The parameter interval can be long.