An actual W phase: CRT peeling and reciprocal inversion

This is the first reciprocal step of Fouvry (1984), p. 238, (8.14), applied to the existing product CRT residue. The moduli q,r need not be coprime. The peeled factor k is coprime to its complement in their lcm. No five-gcd decomposition, small-modulus bound, or estimate for the finite remainder is asserted here. In particular the complementary phase has not been discarded.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhaseInverse (n m : ℕ) : ℤ

Signed Bezout representative of the inverse of n modulo m.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhaseInverse n m = n.gcdA m

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhaseInverse_spec {n m : ℕ} (h : n.Coprime m) : ↑n * wPhaseInverse n m ≡ 1 [ZMOD ↑m]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhase_circle_eq_of_modEq {m : ℕ} (hm : 0 < m) {x y : ℤ} (h : x ≡ y [ZMOD ↑m]) : ↑(↑x / ↑m) = ↑(↑y / ↑m)

Integer congruences give equal normalized phases, also for modulus one.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhase_reciprocity_of_product_congruence {n k : ℕ} (hn : 0 < n) (hk : 0 < k) (hc : n.Coprime k) {a b : ℤ} (hb : b * ↑n ≡ a [ZMOD ↑k]) : ↑(↑b / ↑k) = ↑(↑a / (↑n * ↑k) - ↑a * ↑(wPhaseInverse k n) / ↑n)

Reciprocal inversion with an arbitrary signed numerator and an actual congruence. This is b/k = a/(n*k) - a*bar(k)/n (mod 1).

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhase_circle_peel {n k P : ℕ} (hn : 0 < n) (hk : 0 < k) (hP : 0 < P) (hkP : k.Coprime P) (hnk : n.Coprime k) {a b : ℤ} (hb : b * ↑n ≡ a [ZMOD ↑k]) : ↑(↑b / (↑k * ↑P)) = ↑(↑b * ↑(wPhaseInverse k P) / ↑P) + ↑(↑a / (↑n * ↑k * ↑P) - ↑a * ↑(wPhaseInverse k (n * P)) / (↑n * ↑P))

A coprime CRT peel followed by reciprocal inversion. The input b is arbitrary; its product congruence, rather than a phase identity, is the premise.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_phase_peel {q r n₁ n₂ k P : ℕ} (hn₁ : 0 < n₁) (hk : 0 < k) (hP : 0 < P) (hL : q.lcm r = k * P) (hkq : k ∣ q) (hkP : k.Coprime P) (hc : WCompatible q r n₁ n₂) (a : ℤ) : ↑(↑(productCRTResidue q r n₁ n₂ a) / ↑(q.lcm r)) = ↑(↑(productCRTResidue q r n₁ n₂ a) * ↑(wPhaseInverse k P) / ↑P) + ↑(↑a / (↑n₁ * ↑(q.lcm r)) - ↑a * ↑(wPhaseInverse k (n₁ * P)) / (↑n₁ * ↑P))

The reciprocal peel of the original, constructed W residue. Neither coprimality of q,r nor reducedness of the signed residue a is imposed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_fourier_peel {q r n₁ n₂ k P : ℕ} (hn₁ : 0 < n₁) (hk : 0 < k) (hP : 0 < P) (hL : q.lcm r = k * P) (hkq : k ∣ q) (hkP : k.Coprime P) (hc : WCompatible q r n₁ n₂) (a h : ℤ) : (fourier h) ↑(↑(productCRTResidue q r n₁ n₂ a) / ↑(q.lcm r)) = (fourier h) ↑(↑(productCRTResidue q r n₁ n₂ a) * ↑(wPhaseInverse k P) / ↑P) * (fourier h) ↑(↑a / (↑n₁ * ↑(q.lcm r))) * (fourier h) ↑(-(↑a * ↑(wPhaseInverse k (n₁ * P)) / (↑n₁ * ↑P)))

The actual Fourier phase has a complementary CRT factor, a slow real factor, and a reciprocal factor. The complementary modulus is P, not yet the small modulus D of the five-gcd decomposition.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPeeledPoissonFrequency (M : ℝ) (a : ℤ) (q r n₁ n₂ k P : ℕ) (h : ℤ) : ℂ

A reciprocal representation of the actual frequency, not a replacement by its absolute value. All three phase factors and the zero cutoff remain.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPeeledPoissonFrequency M a q r n₁ n₂ k P h = if h = 0 then 0 else (M / ↑(q.lcm r)) • (FourierTransform.fourier MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffSchwartz) (M / ↑(q.lcm r) * ↑h) * (fourier h) ↑(↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue q r n₁ n₂ a) * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhaseInverse k P) / ↑P) * (fourier h) ↑(↑a / (↑n₁ * ↑(q.lcm r))) * (fourier h) ↑(-(↑a * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhaseInverse k (n₁ * P)) / (↑n₁ * ↑P)))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_eq_peeled {q r n₁ n₂ k P : ℕ} (hn₁ : 0 < n₁) (hk : 0 < k) (hP : 0 < P) (hL : q.lcm r = k * P) (hkq : k ∣ q) (hkP : k.Coprime P) (hc : WCompatible q r n₁ n₂) (M : ℝ) (a h : ℤ) : wPoissonFrequency M a q r n₁ n₂ h = wPeeledPoissonFrequency M a q r n₁ n₂ k P h

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.truncatedWNonzeroMode_eq_peeled (M : ℝ) (H k P : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hN : ∀ n ∈ N, 0 < n) (hfac : ∀ q ∈ reducedModuli Q a, ∀ r ∈ reducedModuli Q a, 0 < k q r ∧ 0 < P q r ∧ q.lcm r = k q r * P q r ∧ k q r ∣ q ∧ (k q r).Coprime (P q r)) : truncatedWNonzeroMode M H N Q β c a = ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, ∑ n₁ ∈ N, ∑ n₂ ∈ N, if WCompatible q r n₁ n₂ then c q * c r * β n₁ * β n₂ * (∑ h ∈ Finset.Icc (-↑(H q r)) ↑(H q r), wPeeledPoissonFrequency M a q r n₁ n₂ (k q r) (P q r) h).re else 0

Exact propagation to the existing retained finite W remainder. The factorization depends only on the modulus pair, and signed coefficients are untouched. No coprimality between the original two moduli is required.