The canonical five-gcd coordinates of W

Fouvry (1984), pp. 235--237, before any large-factor terms are discarded. The five outer coordinates are d,d₁,δ,δ₁,δ₂. The four remaining coordinates recover the original moduli and beta indices exactly.

structure MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData : Type

• d : ℕ
• d₁ : ℕ
• δ : ℕ
• δ₁ : ℕ
• δ₂ : ℕ
• k₁ : ℕ
• k₂ : ℕ
• n₁ : ℕ
• n₂ : ℕ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.ext_iff {x y : WGCDData} : x = y ↔ x.d = y.d ∧ x.d₁ = y.d₁ ∧ x.δ = y.δ ∧ x.δ₁ = y.δ₁ ∧ x.δ₂ = y.δ₂ ∧ x.k₁ = y.k₁ ∧ x.k₂ = y.k₂ ∧ x.n₁ = y.n₁ ∧ x.n₂ = y.n₂

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.ext {x y : WGCDData} (d : x.d = y.d) (d₁ : x.d₁ = y.d₁) (δ : x.δ = y.δ) (δ₁ : x.δ₁ = y.δ₁) (δ₂ : x.δ₂ = y.δ₂) (k₁ : x.k₁ = y.k₁) (k₂ : x.k₂ = y.k₂) (n₁ : x.n₁ = y.n₁) (n₂ : x.n₂ = y.n₂) : x = y

@[instance_reducible]

instance MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.instDecidableEqWGCDData : DecidableEq WGCDData

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.instDecidableEqWGCDData = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.instDecidableEqWGCDData.decEq

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.instDecidableEqWGCDData.decEq (x✝ x✝¹ : WGCDData) : Decidable (x✝ = x✝¹)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.instDecidableEqWGCDData.decEq { d := a, d₁ := a_1, δ := a_2, δ₁ := a_3, δ₂ := a_4, k₁ := a_5, k₂ := a_6, n₁ := a_7, n₂ := a_8 } { d := b, d₁ := b_1, δ := b_2, δ₁ := b_3, δ₂ := b_4, k₁ := b_5, k₂ := b_6, n₁ := b_7, n₂ := b_8 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ if h : a_2 = b_2 then h ▸ if h : a_3 = b_3 then h ▸ if h : a_4 = b_4 then h ▸ if h : a_5 = b_5 then h ▸ if h : a_6 = b_6 then h ▸ if h : a_7 = b_7 then h ▸ if h : a_8 = b_8 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDData (q r N₁ N₂ : ℕ) : WGCDData

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDData q r N₁ N₂ = { d := N₁.gcd N₂, d₁ := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart (N₁ / N₁.gcd N₂) (N₁.gcd N₂), δ := q.gcd r, δ₁ := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart (q / q.gcd r) (q.gcd r), δ₂ := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart (r / q.gcd r) (q.gcd r), k₁ := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart (q / q.gcd r) (q.gcd r), k₂ := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart (r / q.gcd r) (q.gcd r), n₁ := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart (N₁ / N₁.gcd N₂) (N₁.gcd N₂), n₂ := N₂ / N₁.gcd N₂ }

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.D (v : WGCDData) : ℕ

Equations

• v.D = v.δ * v.δ₁ * v.δ₂

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.D' (v : WGCDData) : ℕ

Equations

• v.D' = v.d * v.d₁ * v.D

structure MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid (v : WGCDData) (q r N₁ N₂ : ℕ) : Prop

Arithmetic facts, not distribution or phase estimates.

• d_pos : 0 < v.d
• d₁_pos : 0 < v.d₁
• δ_pos : 0 < v.δ
• δ₁_pos : 0 < v.δ₁
• δ₂_pos : 0 < v.δ₂
• k₁_pos : 0 < v.k₁
• k₂_pos : 0 < v.k₂
• n₁_pos : 0 < v.n₁
• n₂_pos : 0 < v.n₂
• q_eq : q = v.δ * v.δ₁ * v.k₁
• r_eq : r = v.δ * v.δ₂ * v.k₂
• N₁_eq : N₁ = v.d * v.d₁ * v.n₁
• N₂_eq : N₂ = v.d * v.n₂
• d_eq : v.d = N₁.gcd N₂
• δ_eq : v.δ = q.gcd r
• d₁_support (p : ℕ) : Nat.Prime p → p ∣ v.d₁ → p ∣ v.d
• δ₁_support (p : ℕ) : Nat.Prime p → p ∣ v.δ₁ → p ∣ v.δ
• δ₂_support (p : ℕ) : Nat.Prime p → p ∣ v.δ₂ → p ∣ v.δ
• n₁_d : v.n₁.Coprime v.d
• k₁_δ : v.k₁.Coprime v.δ
• k₂_δ : v.k₂.Coprime v.δ
• n_primitive : (v.d₁ * v.n₁).Coprime v.n₂
• k_primitive : (v.δ₁ * v.k₁).Coprime (v.δ₂ * v.k₂)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDData_valid {q r N₁ N₂ : ℕ} (hq : 0 < q) (hr : 0 < r) (hN₁ : 0 < N₁) (hN₂ : 0 < N₂) : (wGCDData q r N₁ N₂).Valid q r N₁ N₂

The data are constructed for every positive original tuple, with no compatibility, size cutoff, or analytic premise.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.D_pos {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : 0 < v.D

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.D'_pos {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : 0 < v.D'

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.k₁_dvd {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : v.k₁ ∣ q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.k₂_dvd {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : v.k₂ ∣ r

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.k_coprime {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : v.k₁.Coprime v.k₂

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.δ_coprime {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : v.δ₁.Coprime v.δ₂

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.k_D {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : (v.k₁ * v.k₂).Coprime v.D

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.n₁_d₁ {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : v.n₁.Coprime v.d₁

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.n₁_n₂ {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : v.n₁.Coprime v.n₂

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.eq_canonical {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : v = wGCDData q r N₁ N₂

Uniqueness of all nine coordinates, not merely a choice of a compatible factorization. This permits exact finite reindexing without multiplicity.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.N₁_D {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) (hc : WCompatible q r N₁ N₂) : N₁.Coprime v.D

Original compatibility gives the two cross-coprimalities through the common modulus, even when the original moduli are not coprime.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.N₂_D {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) (hc : WCompatible q r N₁ N₂) : N₂.Coprime v.D

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.phase_coprime {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) (hc : WCompatible q r N₁ N₂) : (v.n₁ * v.k₁ * v.k₂).Coprime v.D' ∧ v.k₁.Coprime (v.n₁ * v.k₂) ∧ v.n₂.Coprime (v.n₁ * v.k₂)

All the arithmetic hypotheses of the existing three-factor phase follow from the canonical decomposition and the original W compatibility.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.small_moduli {v : WGCDData} {Y : ℝ} (hY : 0 ≤ Y) (hd : ↑v.d ≤ Y) (hd₁ : ↑v.d₁ ≤ Y) (hδ : ↑v.δ ≤ Y) (hδ₁ : ↑v.δ₁ ≤ Y) (hδ₂ : ↑v.δ₂ ≤ Y) : ↑v.D ≤ Y ^ 3 ∧ ↑v.D' ≤ Y ^ 5

Uniform algebraic small-modulus bounds; no discarded contribution is estimated here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_eq_canonical_threeFactor {q r N₁ N₂ : ℕ} (hq : 0 < q) (hr : 0 < r) (hN₁ : 0 < N₁) (hN₂ : 0 < N₂) (hc : WCompatible q r N₁ N₂) (M : ℝ) (a h : ℤ) : have v := wGCDData q r N₁ N₂; wPoissonFrequency M a q r N₁ N₂ h = wThreeFactorPoissonFrequency M a q r v.d v.d₁ v.D v.k₁ v.k₂ v.n₁ v.n₂ h

The real frequency on every positive compatible original tuple, with all factorization and coprimality premises now constructed.