The small-modulus root of the W phase

Fouvry (1984), p. 237, (8.8), and Fouvry (1987), p. 627, (3.11). The large CRT residue may be replaced, modulo D, by the CRT on the two small moduli. The resulting root phase is constant on explicit congruence classes; no equality of chosen integer representatives is asserted.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible.of_dvd {q r p s N₁ N₂ : ℕ} (hc : WCompatible q r N₁ N₂) (hp : p ∣ q) (hs : s ∣ r) : WCompatible p s N₁ N₂

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_restrict {q r p s N₁ N₂ : ℕ} (hc : WCompatible q r N₁ N₂) (hp : p ∣ q) (hs : s ∣ r) (a : ℤ) : productCRTResidue q r N₁ N₂ a ≡ productCRTResidue p s N₁ N₂ a [ZMOD ↑(p.lcm s)]

Restriction of the actual constructed CRT representative.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_congr {p s N₁ N₂ N₁' N₂' : ℕ} (hc : WCompatible p s N₁ N₂) (hc' : WCompatible p s N₁' N₂') (h₁ : N₁ ≡ N₁' [MOD p]) (h₂ : N₂ ≡ N₂' [MOD s]) (a : ℤ) : productCRTResidue p s N₁ N₂ a ≡ productCRTResidue p s N₁' N₂' a [ZMOD ↑(p.lcm s)]

Changing the two multipliers within their residue classes only changes the chosen representative by a multiple of the lcm.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhaseInverse_congr {u v m : ℕ} (hu : u.Coprime m) (hv : v.Coprime m) (h : u ≡ v [MOD m]) : wPhaseInverse u m ≡ wPhaseInverse v m [ZMOD ↑m]

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smallWCRTResidue (d d₁ δ δ₁ δ₂ n₁ n₂ : ℕ) (a : ℤ) : ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smallWCRTResidue d d₁ δ δ₁ δ₂ n₁ n₂ a = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue (δ * δ₁) (δ * δ₂) (d * d₁ * n₁) (d * n₂) a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.small_lcm {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : (v.δ * v.δ₁).lcm (v.δ * v.δ₂) = v.D

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.small_compatible {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) (hc : WCompatible q r N₁ N₂) : WCompatible (v.δ * v.δ₁) (v.δ * v.δ₂) (v.d * v.d₁ * v.n₁) (v.d * v.n₂)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.residue_modEq_small {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) (hc : WCompatible q r N₁ N₂) (a : ℤ) : productCRTResidue q r N₁ N₂ a ≡ smallWCRTResidue v.d v.d₁ v.δ v.δ₁ v.δ₂ v.n₁ v.n₂ a [ZMOD ↑v.D]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smallWCRTResidue_congr {d d₁ δ δ₁ δ₂ n₁ n₂ n₁' n₂' : ℕ} (hδ : δ₁.Coprime δ₂) (hc : WCompatible (δ * δ₁) (δ * δ₂) (d * d₁ * n₁) (d * n₂)) (hc' : WCompatible (δ * δ₁) (δ * δ₂) (d * d₁ * n₁') (d * n₂')) (h₁ : n₁ ≡ n₁' [MOD δ * δ₁ * δ₂]) (h₂ : n₂ ≡ n₂' [MOD δ * δ₁ * δ₂]) (a : ℤ) : smallWCRTResidue d d₁ δ δ₁ δ₂ n₁ n₂ a ≡ smallWCRTResidue d d₁ δ δ₁ δ₂ n₁' n₂' a [ZMOD ↑δ * ↑δ₁ * ↑δ₂]

The actual small CRT root depends only on the two beta coordinates modulo D, for fixed outer coordinates.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSmallRootPhase (d d₁ δ δ₁ δ₂ k₁ k₂ n₁ n₂ : ℕ) (a : ℤ) : UnitAddCircle

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSmallRootPhase d d₁ δ δ₁ δ₂ k₁ k₂ n₁ n₂ a = ↑(↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smallWCRTResidue d d₁ δ δ₁ δ₂ n₁ n₂ a) * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhaseInverse (k₁ * k₂) (δ * δ₁ * δ₂)) / ↑(δ * δ₁ * δ₂) - ↑a * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPhaseInverse (n₁ * k₁ * k₂) (d * d₁ * (δ * δ₁ * δ₂))) / ↑(d * d₁ * (δ * δ₁ * δ₂)))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.rootPhase_eq {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) (hc : WCompatible q r N₁ N₂) (a : ℤ) : ↑(↑(productCRTResidue q r N₁ N₂ a) * ↑(wPhaseInverse (v.k₁ * v.k₂) v.D) / ↑v.D - ↑a * ↑(wPhaseInverse (v.n₁ * v.k₁ * v.k₂) v.D') / ↑v.D') = wSmallRootPhase v.d v.d₁ v.δ v.δ₁ v.δ₂ v.k₁ v.k₂ v.n₁ v.n₂ a

Replacement of the complementary root in the actual W phase.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_phase_smallRoot {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) (hc : WCompatible q r N₁ N₂) (a : ℤ) : ↑(↑(productCRTResidue q r N₁ N₂ a) / ↑(q.lcm r)) = wSmallRootPhase v.d v.d₁ v.δ v.δ₁ v.δ₂ v.k₁ v.k₂ v.n₁ v.n₂ a + ↑(↑a / (↑v.n₁ * ↑v.k₁ * ↑v.k₂ * ↑v.D')) + ↑(↑a * (↑v.d₁ * ↑v.n₁ - ↑v.n₂) * ↑(wPhaseInverse (v.D' * v.n₂ * v.k₁) (v.n₁ * v.k₂)) / (↑v.n₁ * ↑v.k₂))

The entire original phase with its root replaced by a genuinely small-modulus CRT, ready for freezing before partial summation.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSmallRootPhase_congr {d d₁ δ δ₁ δ₂ k₁ k₂ k₁' k₂' n₁ n₂ n₁' n₂' : ℕ} (hd : 0 < d) (hd₁ : 0 < d₁) (hD : 0 < δ * δ₁ * δ₂) (hδ : δ₁.Coprime δ₂) (hc : WCompatible (δ * δ₁) (δ * δ₂) (d * d₁ * n₁) (d * n₂)) (hc' : WCompatible (δ * δ₁) (δ * δ₂) (d * d₁ * n₁') (d * n₂')) (hk : (k₁ * k₂).Coprime (δ * δ₁ * δ₂)) (hk' : (k₁' * k₂').Coprime (δ * δ₁ * δ₂)) (hnk : (n₁ * k₁ * k₂).Coprime (d * d₁ * (δ * δ₁ * δ₂))) (hnk' : (n₁' * k₁' * k₂').Coprime (d * d₁ * (δ * δ₁ * δ₂))) (hn₁ : n₁ ≡ n₁' [MOD d * d₁ * (δ * δ₁ * δ₂)]) (hn₂ : n₂ ≡ n₂' [MOD δ * δ₁ * δ₂]) (hkk : k₁ * k₂ ≡ k₁' * k₂' [MOD d * d₁ * (δ * δ₁ * δ₂)]) (a : ℤ) : wSmallRootPhase d d₁ δ δ₁ δ₂ k₁ k₂ n₁ n₂ a = wSmallRootPhase d d₁ δ δ₁ δ₂ k₁' k₂' n₁' n₂' a

Freeze the small root by fixing residue classes. The first inverse uses the modulus D; the second uses D'=d*d₁*D.