Exact five-gcd reindexing of the retained W sum

All finite supports, signed coefficients, and frequencies are preserved. The large-factor contribution is split off explicitly, not declared negligible.

@[reducible, inline]

abbrev MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WOriginalTuple : Type

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WOriginalTuple = ((ℕ × ℕ) × ℕ × ℕ)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.original (v : WGCDData) : WOriginalTuple

Equations

• v.original = ((v.δ * v.δ₁ * v.k₁, v.δ * v.δ₂ * v.k₂), v.d * v.d₁ * v.n₁, v.d * v.n₂)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (t : WOriginalTuple) : WGCDData

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple t = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDData t.1.1 t.1.2 t.2.1 t.2.2

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple_original {t : WOriginalTuple} (ht : 0 < t.1.1 ∧ 0 < t.1.2 ∧ 0 < t.2.1 ∧ 0 < t.2.2) : (wGCDTuple t).original = t

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalTuples (N Q : Finset ℕ) (a : ℤ) : Finset WOriginalTuple

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalTuples N Q a = {t ∈ (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a ×ˢ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a) ×ˢ N ×ˢ N | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible t.1.1 t.1.2 t.2.1 t.2.2}

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuples (N Q : Finset ℕ) (a : ℤ) : Finset WGCDData

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuples N Q a = Finset.image MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalTuples N Q a)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalTuples_pos {N Q : Finset ℕ} {a : ℤ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {t : WOriginalTuple} (ht : t ∈ wOriginalTuples N Q a) : 0 < t.1.1 ∧ 0 < t.1.2 ∧ 0 < t.2.1 ∧ 0 < t.2.2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple_injOn {N Q : Finset ℕ} {a : ℤ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) : Set.InjOn wGCDTuple ↑(wOriginalTuples N Q a)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wGCDTuples_iff {N Q : Finset ℕ} {a : ℤ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) (v : WGCDData) : v ∈ wGCDTuples N Q a ↔ v.original ∈ wOriginalTuples N Q a ∧ v.Valid v.original.1.1 v.original.1.2 v.original.2.1 v.original.2.2

The image domain is characterized by genuine arithmetic validity and membership of the reconstructed original tuple, with no chosen witnesses.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGCDTuples {A : Type u_1} [AddCommMonoid A] {N Q : Finset ℕ} {a : ℤ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) (f : WGCDData → A) : ∑ v ∈ wGCDTuples N Q a, f v = ∑ t ∈ wOriginalTuples N Q a, f (wGCDTuple t)

An exact change of variables for arbitrary additive weights.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalTerm (M : ℝ) (H : ℕ → ℕ → ℕ) (β c : ℕ → ℝ) (a : ℤ) (t : WOriginalTuple) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wOriginalTerm M H β c a t = c t.1.1 * c t.1.2 * β t.2.1 * β t.2.2 * (∑ h ∈ Finset.Icc (-↑(H t.1.1 t.1.2)) ↑(H t.1.1 t.1.2), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency M a t.1.1 t.1.2 t.2.1 t.2.2 h).re

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.truncatedWNonzeroMode_eq_originalTuples (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : truncatedWNonzeroMode M H N Q β c a = ∑ t ∈ wOriginalTuples N Q a, wOriginalTerm M H β c a t

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTerm (M : ℝ) (H : ℕ → ℕ → ℕ) (β c : ℕ → ℝ) (a : ℤ) (v : WGCDData) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTerm M H β c a v = c v.original.1.1 * c v.original.1.2 * β v.original.2.1 * β v.original.2.2 * (∑ h ∈ Finset.Icc (-↑(H v.original.1.1 v.original.1.2)) ↑(H v.original.1.1 v.original.1.2), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wThreeFactorPoissonFrequency M a v.original.1.1 v.original.1.2 v.d v.d₁ v.D v.k₁ v.k₂ v.n₁ v.n₂ h).re

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTerm_eq_originalTerm {t : WOriginalTuple} (ht : 0 < t.1.1 ∧ 0 < t.1.2 ∧ 0 < t.2.1 ∧ 0 < t.2.2) (hc : WCompatible t.1.1 t.1.2 t.2.1 t.2.2) (M : ℝ) (H : ℕ → ℕ → ℕ) (β c : ℕ → ℝ) (a : ℤ) : wGCDTerm M H β c a (wGCDTuple t) = wOriginalTerm M H β c a t

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.truncatedWNonzeroMode_eq_gcdTuples (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) : truncatedWNonzeroMode M H N Q β c a = ∑ v ∈ wGCDTuples N Q a, wGCDTerm M H β c a v

The actual signed finite W remainder, now in canonical coordinates. No coprimality or factorization hypotheses are supplied by the caller.

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

Equations

• v.key = (v.d, v.d₁, v.δ, v.δ₁, v.δ₂)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.truncatedWNonzeroMode_eq_fiveGCD (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) : truncatedWNonzeroMode M H N Q β c a = ∑ z ∈ Finset.image WGCDData.key (wGCDTuples N Q a), ∑ v ∈ wGCDTuples N Q a with v.key = z, wGCDTerm M H β c a v

Exact five-parameter outer grouping. The inner fibers still contain all four free coordinates and all original support conditions.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Small (v : WGCDData) (Y : ℝ) : Prop

Equations

• v.Small Y = (↑v.d ≤ Y ∧ ↑v.d₁ ≤ Y ∧ ↑v.δ ≤ Y ∧ ↑v.δ₁ ≤ Y ∧ ↑v.δ₂ ≤ Y)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Small.moduli {v : WGCDData} {Y : ℝ} (hY : 0 ≤ Y) (hv : v.Small Y) : ↑v.D ≤ Y ^ 3 ∧ ↑v.D' ≤ Y ^ 5

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDSmallSum (M Y : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDSmallSum M Y H N Q β c a = ∑ v ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuples N Q a with v.Small Y, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTerm M H β c a v

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDLargeSum (M Y : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDLargeSum M Y H N Q β c a = ∑ v ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuples N Q a with ¬v.Small Y, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTerm M H β c a v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.truncatedWNonzeroMode_eq_small_add_large (M Y : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) : truncatedWNonzeroMode M H N Q β c a = wGCDSmallSum M Y H N Q β c a + wGCDLargeSum M Y H N Q β c a

A signed equality with the discarded contribution still present.