Uniform logarithmic payment of the small-gcd zero-mode difference

Siegel--Walfisz is a hypothesis on a given family, not a property asserted for arbitrary beta. Its constant is chosen before the family member and all AP moduli, coprime sieves, and residues. The threshold below is likewise chosen before the member, scales, supports, and signed modulus weights. The large-gcd term remains outside these estimates.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.BetaCoprimeSWFamily {ι : Type u_1} (κ : ℕ) (T : ι → ℝ) (N : ι → Finset ℕ) (β : ι → ℕ → ℝ) : Prop

The family-uniform, independently coprime-sieved beta-SW input. The sieve order is fixed; the saving exponent and its constant precede every changing family member and every arithmetic parameter.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.BetaCoprimeSWFamily κ T N β = ∀ (B : ℕ), ∃ (C : ℝ), 0 < C ∧ ∀ (i : ι) (d h : ℕ), 0 < d → 0 < h → ∀ (b : ℕ), b.Coprime d → |MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCoprimeAPDiscrepancy (N i) (β i) d h b| ≤ C * T i * ↑((MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau κ) h) / Real.log (2 * T i) ^ B

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.BetaCoprimeSWFamily.double_scale {ι : Type u_1} {κ : ℕ} {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (i : ι), 1 ≤ T i) : BetaCoprimeSWFamily κ (fun (i : ι) => 2 * T i) N β

Passing from the lower dyadic scale to the upper support endpoint does not strengthen the SW input: its constant grows by the fixed factor 2^B.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWUSmallDelta_abs_le_SW {k : ℕ} (hk : 1 ≤ k) (j κ B : ℕ) {T L D C : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (hD : 0 ≤ D) (hC : 0 ≤ C) (M : ℝ) (N Q : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (β c : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) (hSW : ∀ (d h : ℕ), 0 < d → 0 < h → ∀ (b : ℕ), b.Coprime d → |betaCoprimeAPDiscrepancy N β d h b| ≤ C * T * ↑((fouvryTau κ) h) / Real.log (2 * T) ^ B) : |smoothWUSmallDelta M D N Q β c a| ≤ 2 * |M * dyadicCutoffMass| * C * T ^ 2 * ((1 + Real.log T) ^ (k - 1) * D * (1 + Real.log L) ^ (j * (κ + 2)) / Real.log (2 * T) ^ B)

The explicit SW small-gcd bound, retaining the original sieve order.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smallDelta_log_budget (p s d A : ℕ) {x T L D ε : ℝ} (hx : 1 ≤ Real.log x) (hx0 : 0 < x) (hT : 1 ≤ T) (hL : 1 ≤ L) (hTx : T ≤ x) (hLx : L ≤ x) (hε : 0 < ε) (hεT : x ^ ε ≤ T) (hD : 0 ≤ D) (hDx : D ≤ Real.log x ^ d) : (1 + Real.log T) ^ p * D * (1 + Real.log L) ^ s / Real.log (2 * T) ^ (A + (p + s + d)) ≤ 2 ^ (p + s) / ε ^ (A + (p + s + d)) / Real.log x ^ A

Elementary logarithm accounting at T ≥ x^ε. The saving order is explicitly the desired order plus the beta/modulus/delta logarithm costs.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWUSmallDelta_SWFamily_log_payment {ι : Type u_1} {κ k : ℕ} (hk : 1 ≤ k) (j d A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (i : ι), 1 ≤ T i) (hN : ∀ (i : ι), N i ⊆ Finset.Ioc 0 ⌊T i⌋₊) (hβ : ∀ (i : ι), ∀ n ∈ N i, |β i n| ≤ ↑((fouvryTau k) n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (i : ι), T i ≤ x → x ^ ε ≤ T i → ∀ (M L D : ℝ), 1 ≤ L → L ≤ x → 0 ≤ D → D ≤ Real.log x ^ d → ∀ Q ⊆ Finset.Ioc 0 ⌊L⌋₊, ∀ (c : ℕ → ℝ), (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |smoothWUSmallDelta M D (N i) Q (β i) c a| ≤ |M| * T i ^ 2 / Real.log x ^ A

Genuine uniform log saving for the small-gcd part of W zero minus U zero, in the natural |M| T² normalization. The threshold depends on the given family SW constants and fixed orders, never on the family member or residue. No relation between M and x is needed for this stronger normalized form.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.alpha_sq_mul_smoothWU_sub_large_SWFamily_log_payment {ι : Type u_1} {κ k ℓ : ℕ} (hk : 1 ≤ k) (hℓ : 1 ≤ ℓ) (j d A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (i : ι), 1 ≤ T i) (hN : ∀ (i : ι), N i ⊆ Finset.Ioc 0 ⌊T i⌋₊) (hβ : ∀ (i : ι), ∀ n ∈ N i, |β i n| ≤ ↑((fouvryTau k) n)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (i : ι) (M L D : ℝ), 1 ≤ M → 1 ≤ L → M * T i ≤ x → L ≤ x → x ^ ε ≤ T i → 0 ≤ D → D ≤ Real.log x ^ d → ∀ (S Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau ℓ) m)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), (∑ m ∈ S, α m ^ 2) * |smoothWMain M (N i) Q (β i) c a - smoothUMain M (N i) Q (β i) c a - smoothWULargeDelta M D (N i) Q (β i) c a| ≤ x ^ 2 / Real.log x ^ A

After the actual alpha second moment, the small-gcd part is paid at x² / log(x)^A whenever M T ≤ x and T ≥ x^ε. The statement uses the actual W-minus-U zero modes minus their explicit large-gcd remainder. It makes no assertion that this remaining large-gcd term is small.