The full, unpruned W zero frequency

This is the signed finite expansion of Fouvry (1984), p. 235, (8.1), followed by CRT and exact Poisson extraction. It supplies the zero-frequency content underlying p. 238, (8.11), before any truncation or five-gcd pruning. It does not identify the raw main term with the already-pruned expression (8.11). The oscillatory remainder is retained. The crude uniform coefficient envelope is not the Fouvry (1987) distribution estimate. No WF/SW or spectral estimate is used, and neither (8.25) nor (9.1) is imported.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.product_modEq_iff_of_coprime {q n : ℕ} (hn : n.Coprime q) {a b m : ℤ} (hb : b * ↑n ≡ a [ZMOD ↑q]) : m * ↑n ≡ a [ZMOD ↑q] ↔ m ≡ b [ZMOD ↑q]

Cancellation uses a genuine Bezout inverse, including for integer operands.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.product_congruences_compatible {q r n₁ n₂ : ℕ} (hq : 0 < q) {a m : ℤ} (ha : a.gcd ↑q = 1) (h₁ : m * ↑n₁ ≡ a [ZMOD ↑q]) (h₂ : m * ↑n₂ ≡ a [ZMOD ↑r]) : n₁ ≡ n₂ [MOD q.gcd r]

A common integer solution forces equality of the multipliers modulo the gcd. Only reducedness modulo q is needed for this direction.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.exists_product_crt_residue {q r n₁ n₂ : ℕ} (h₁ : n₁.Coprime q) (h₂ : n₂.Coprime r) (hc : n₁ ≡ n₂ [MOD q.gcd r]) (a : ℤ) : ∃ (b : ℤ), b * ↑n₁ ≡ a [ZMOD ↑q] ∧ b * ↑n₂ ≡ a [ZMOD ↑r] ∧ ∀ (m : ℤ), m * ↑n₁ ≡ a [ZMOD ↑q] ∧ m * ↑n₂ ≡ a [ZMOD ↑r] ↔ m ≡ b [ZMOD ↑(q.lcm r)]

General (not necessarily coprime-modulus) CRT constructs the multiplier first; its Bezout inverse constructs an actual common product residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.exists_product_congruences_iff {q r n₁ n₂ : ℕ} (hq : 0 < q) (h₁ : n₁.Coprime q) (h₂ : n₂.Coprime r) {a : ℤ} (ha : a.gcd ↑q = 1) : (∃ (m : ℤ), m * ↑n₁ ≡ a [ZMOD ↑q] ∧ m * ↑n₂ ≡ a [ZMOD ↑r]) ↔ n₁ ≡ n₂ [MOD q.gcd r]

Solvability over all integers is exactly the gcd compatibility condition.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productProgressionWeight (S : Finset ℕ) (w : ℕ → ℝ) (a : ℤ) (q r n₁ n₂ : ℕ) : ℝ

The original, unpruned inner sum in (8.1).

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productProgressionWeight S w a q r n₁ n₂ = ∑ m ∈ S, if ↑m * ↑n₁ ≡ a [ZMOD ↑q] ∧ ↑m * ↑n₂ ≡ a [ZMOD ↑r] then w m else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productProgressionWeight_eq_zero_of_incompatible (S : Finset ℕ) (w : ℕ → ℝ) {q r n₁ n₂ : ℕ} (hq : 0 < q) {a : ℤ} (ha : a.gcd ↑q = 1) (hc : ¬n₁ ≡ n₂ [MOD q.gcd r]) : productProgressionWeight S w a q r n₁ n₂ = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionW_eq_product_progression_sum (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) : dispersionW S N Q w β c a = ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, ∑ n₁ ∈ N, ∑ n₂ ∈ N, if n₁.Coprime q ∧ n₂.Coprime r then c q * c r * β n₁ * β n₂ * productProgressionWeight S w a q r n₁ n₂ else 0

Literal expansion of the actual signed dispersion W, before gcd pruning or frequency truncation. Both necessary multiplier coprimalities are retained.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible (q r n₁ n₂ : ℕ) : Prop

Exactly the arithmetic restrictions forced by the two product congruences.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible q r n₁ n₂ = (n₁.Coprime q ∧ n₂.Coprime r ∧ n₁ ≡ n₂ [MOD q.gcd r])

@[instance_reducible]

instance MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCompatibleDecidable (q r n₁ n₂ : ℕ) : Decidable (WCompatible q r n₁ n₂)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCompatibleDecidable q r n₁ n₂ = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCompatibleDecidable._aux_1 q r n₁ n₂

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue (q r n₁ n₂ : ℕ) (a : ℤ) : ℤ

A representative chosen from the proved CRT construction, not a supplied progression-representation premise. Its value on incompatible inputs is unused.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue q r n₁ n₂ a = if h : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible q r n₁ n₂ then Classical.choose ⋯ else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_spec {q r n₁ n₂ : ℕ} (a : ℤ) (hc : WCompatible q r n₁ n₂) : productCRTResidue q r n₁ n₂ a * ↑n₁ ≡ a [ZMOD ↑q] ∧ productCRTResidue q r n₁ n₂ a * ↑n₂ ≡ a [ZMOD ↑r] ∧ ∀ (m : ℤ), m * ↑n₁ ≡ a [ZMOD ↑q] ∧ m * ↑n₂ ≡ a [ZMOD ↑r] ↔ m ≡ productCRTResidue q r n₁ n₂ a [ZMOD ↑(q.lcm r)]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productProgressionWeight_eq_crt_progression (S : Finset ℕ) (w : ℕ → ℝ) (a : ℤ) {q r n₁ n₂ : ℕ} (hc : WCompatible q r n₁ n₂) : productProgressionWeight S w a q r n₁ n₂ = ∑ m ∈ S, if ↑m ≡ productCRTResidue q r n₁ n₂ a [ZMOD ↑(q.lcm r)] then w m else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionW_eq_compatible_sum (S N Q : Finset ℕ) (w β c : ℕ → ℝ) (a : ℤ) (hQ : ∀ q ∈ Q, q ≠ 0) : dispersionW S N Q w β 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₂ * productProgressionWeight S w a q r n₁ n₂ else 0

Incompatible pairs vanish identically; no estimated or pruned term is lost.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_progression_eq_main_add_fourier {M : ℝ} (hM : 0 < M) {q : ℕ} (hq : 0 < q) (b : ℤ) : (∑ m ∈ dyadicCutoffNatSupport M, if ↑m ≡ b [ZMOD ↑q] then scaledDyadicCutoff M ↑m else 0) = M / ↑q * dyadicCutoffMass + (∑' (h : ℤ), dyadicCutoffPoissonRemainder (M / ↑q) (↑b / ↑q) h).re

The real finite progression identity with its full oscillatory error.

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

The phase uses the actual constructed CRT residue modulo the lcm.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency M a q r n₁ n₂ h = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffPoissonRemainder (M / ↑(q.lcm r)) (↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue q r n₁ n₂ a) / ↑(q.lcm r)) h

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_zero (M : ℝ) (a : ℤ) (q r n₁ n₂ : ℕ) : wPoissonFrequency M a q r n₁ n₂ 0 = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_summable_norm {M : ℝ} (hM : 0 < M) (a : ℤ) {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) (n₁ n₂ : ℕ) : Summable fun (h : ℤ) => ‖wPoissonFrequency M a q r n₁ n₂ h‖

Absolute convergence holds without a modulus-versus-scale restriction.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productProgressionWeight_eq_main_add_fourier {M : ℝ} (hM : 0 < M) (a : ℤ) {q r n₁ n₂ : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) (hc : WCompatible q r n₁ n₂) : productProgressionWeight (dyadicCutoffNatSupport M) (fun (m : ℕ) => scaledDyadicCutoff M ↑m) a q r n₁ n₂ = M / ↑(q.lcm r) * dyadicCutoffMass + (∑' (h : ℤ), wPoissonFrequency M a q r n₁ n₂ h).re

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

The full raw zero mode; all original coefficient signs are retained. No five-gcd restrictions or truncation errors have yet been introduced.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWMain M N Q β c a = M * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffMass * ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ r ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, c q * c r / ↑(q.lcm r) * ∑ n₁ ∈ N, ∑ n₂ ∈ N, if MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible q r n₁ n₂ then β n₁ * β n₂ else 0

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

An exact nonzero-frequency remainder, not an absolute-value substitute.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWNonzeroMode M N Q β c a = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ r ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ n₁ ∈ N, ∑ n₂ ∈ N, if MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible q r n₁ n₂ then c q * c r * β n₁ * β n₂ * (∑' (h : ℤ), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency M a q r n₁ n₂ h).re else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWMain_eq_compatible_sum (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : smoothWMain M 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₂ * (M / ↑(q.lcm r) * dyadicCutoffMass) else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionW_eq_smoothWMain_add_nonzeroMode {M : ℝ} (hM : 0 < M) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hQ : ∀ q ∈ Q, q ≠ 0) : dispersionW (dyadicCutoffNatSupport M) N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a = smoothWMain M N Q β c a + smoothWNonzeroMode M N Q β c a

Exact full W = raw zero mode + the CRT-phase nonzero Fourier remainder. The residue a is arbitrary and may vary with all other inputs.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWErrorEnvelope (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : ℝ

The unpruned absolute coefficient envelope. Its growth is not estimated.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWErrorEnvelope N Q β c a = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ r ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ n₁ ∈ N, ∑ n₂ ∈ N, if MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible q r n₁ n₂ then |c q * c r * β n₁ * β n₂| else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWErrorEnvelope_nonneg (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : 0 ≤ smoothWErrorEnvelope N Q β c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dispersionW_smooth_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ), (∀ q ∈ Q, q ≠ 0) → |dispersionW (dyadicCutoffNatSupport M) N Q (fun (m : ℕ) => scaledDyadicCutoff M ↑m) β c a - smoothWMain M N Q β c a| ≤ C * smoothWErrorEnvelope N Q β c a

A universal coarse error bound, chosen before every arithmetic input. This is not sufficient for the F87 distribution theorem: the exact oscillatory remainder above still needs cancellation estimates.