The same-first-index reciprocal correlation in F87 IV.3

Fouvry (1987), p. 632, (4.7)--(4.8). The two phases share n, not just d₁ and r. Their common modulus is n*r*s*s', with no second copy of n. The factors s,s' need not be coprime. Signed frequencies and residue, zero correlation numerator, and modulus one are all retained.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalCircle (q u : ℕ) (A : ℤ) : UnitAddCircle

The unmasked reciprocal circle phase, with the existing Bezout inverse.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalCircle q u A = ↑(↑(A * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhaseInverse u q) / ↑q)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalPhase (D d₁ n n₂ k r s : ℕ) (a : ℤ) : UnitAddCircle

F87's original phase, after k₂ = r*s.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalPhase D d₁ n n₂ k r s a = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalCircle (n * r * s) (D * n₂ * k) (a * (↑d₁ * ↑n - ↑n₂))

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator (d₁ n n₂ n₂' s s' : ℕ) (a h h' : ℤ) : ℤ

The signed integer in (4.8); both differences have the same n.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' = a * (h * ↑n₂' * ↑s' * (↑d₁ * ↑n - ↑n₂) - h' * ↑n₂ * ↑s * (↑d₁ * ↑n - ↑n₂'))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wReciprocalPhase_eq_iv3 {v : WGCDData} {r s : ℕ} (hfactor : v.k₂ = r * s) (a : ℤ) : wReciprocalPhase v a = iv3ReciprocalPhase v.D' v.d₁ v.n₁ v.n₂ v.k₁ r s a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalCircle_fourier (q u : ℕ) (A h : ℤ) : (fourier h) (iv3ReciprocalCircle q u A) = (fourier 1) (iv3ReciprocalCircle q u (h * A))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_inverse_transport {m j u v : ℕ} (hc : (u * v).Coprime (m * j)) : wPhaseInverse u m ≡ ↑v * wPhaseInverse (u * v) (m * j) [ZMOD ↑m]

Inverse transport only uses divisibility of the moduli, not coprimality of their quotient and the smaller modulus.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalCircle_common_denominator {m j u v : ℕ} (hm : 0 < m) (hj : 0 < j) (hc : (u * v).Coprime (m * j)) (A : ℤ) : iv3ReciprocalCircle m u A = iv3ReciprocalCircle (m * j) (u * v) (A * ↑v * ↑j)

Exact passage to a larger denominator and a common inverse.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalCircle_sub (q u : ℕ) (A B : ℤ) : iv3ReciprocalCircle q u A - iv3ReciprocalCircle q u B = iv3ReciprocalCircle q u (A - B)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_reciprocal_correlation {D d₁ n n₂ n₂' k r s s' : ℕ} (hn : 0 < n) (hr : 0 < r) (hs : 0 < s) (hs' : 0 < s') (hc : (D * n₂ * n₂' * k).Coprime (n * r * s * s')) (a h h' : ℤ) : (fourier h) (iv3ReciprocalPhase D d₁ n n₂ k r s a) * star ((fourier h') (iv3ReciprocalPhase D d₁ n n₂' k r s' a)) = (fourier 1) (iv3ReciprocalCircle (n * r * s * s') (D * n₂ * n₂' * k) (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h'))

The exact paired phase in (4.7). The sole coprimality hypothesis is that the common inverse exists. In particular, there is no pairwise-coprimality assumption on n,r,s,s'.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.norm_iv3_reciprocal_correlation (D d₁ n n₂ n₂' k r s s' : ℕ) (a h h' : ℤ) : ‖(fourier h) (iv3ReciprocalPhase D d₁ n n₂ k r s a) * star ((fourier h') (iv3ReciprocalPhase D d₁ n n₂' k r s' a))‖ = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_reciprocal_correlation_zero {D d₁ n n₂ n₂' k r s s' : ℕ} (hn : 0 < n) (hr : 0 < r) (hs : 0 < s) (hs' : 0 < s') (hc : (D * n₂ * n₂' * k).Coprime (n * r * s * s')) (a h h' : ℤ) (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' = 0) : (fourier h) (iv3ReciprocalPhase D d₁ n n₂ k r s a) * star ((fourier h') (iv3ReciprocalPhase D d₁ n n₂' k r s' a)) = 1

The zero-numerator branch is exactly one, not just bounded by one.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_wPhaseInverse_zmod {q u : ℕ} (hc : u.Coprime q) : ↑(wPhaseInverse u q) = (↑u)⁻¹

Agreement with the inverse used by the complete Weil theorem, including the trivial residue ring at modulus one.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalCircle_stdAddChar {q u : ℕ} [NeZero q] (hc : u.Coprime q) (A : ℤ) : (fourier 1) (iv3ReciprocalCircle q u A) = ZMod.stdAddChar (↑A * (↑u)⁻¹)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_gcd_inverse_twist {q u : ℕ} (hc : u.Coprime q) (A : ℤ) : q.gcd (A * wPhaseInverse u q).natAbs = q.gcd A.natAbs

Absorbing a fixed unit into the frequency does not change its gcd with the modulus. This also covers zero and negative frequencies.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ReciprocalCircle_eq_reciprocalPhase {q B k : ℕ} [NeZero q] (hB : B.Coprime q) (hk : k.Coprime q) (A : ℤ) : (fourier 1) (iv3ReciprocalCircle q (B * k) A) = reciprocalPhase q (A * wPhaseInverse B q) ↑k

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

The actual unweighted interval of positive k, with precisely its coprimality restriction. No coefficient or additional carrier mask is present.

Equations

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_reciprocalInterval_nat {q : ℕ} [NeZero q] (d : ℤ) (X Y : ℕ) : ∑ k ∈ Finset.Ioc X Y, reciprocalPhase q d ↑k = reciprocalInterval q d ↑X ↑Y

Natural interval endpoints give the same interval convention as the established Fouvry bound: X < k ≤ Y.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationInterval_eq_reciprocalInterval {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' : ℤ) (X Y : ℕ) : iv3CorrelationInterval D d₁ n n₂ n₂' r s s' a h h' X Y = reciprocalInterval (n * r * s * s') (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' * wPhaseInverse (D * n₂ * n₂') (n * r * s * s')) ↑X ↑Y

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

The unconditional complete Weil theorem applies to this unweighted interval, not to an arbitrarily weighted or further masked correlation.