Family-uniform logarithmic payment of the complete zero-mode difference

The SW input is the existing all-positive-modulus, coprime-sieved family condition. Constants precede all family members, supports, scales, modulus weights and integer residues. The lcm-weight estimate leaves no gcd range unpaid in W zero minus U zero. Nonzero W frequencies are not estimated here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWMain_sub_smoothUMain_abs_le_SW {k : ℕ} (hk : 1 ≤ k) (j κ B : ℕ) {T L C : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (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) : |smoothWMain M N Q β c a - smoothUMain M N Q β c a| ≤ 2 * |M * dyadicCutoffMass| * C * T ^ 2 * ((1 + Real.log T) ^ (k - 1) * (1 + Real.log L) ^ (2 * (j * (κ + 1)) ^ 2 + 1) / Real.log (2 * T) ^ B)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWU_SWFamily_log_payment {ι : Type u_1} {κ k : ℕ} (hk : 1 ≤ k) (j 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 : ℝ), 1 ≤ L → L ≤ x → ∀ Q ⊆ Finset.Ioc 0 ⌊L⌋₊, ∀ (c : ℕ → ℝ), (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |smoothWMain M (N i) Q (β i) c a - smoothUMain M (N i) Q (β i) c a| ≤ |M| * T i ^ 2 / Real.log x ^ A

All gcd ranges are paid in the natural |M| T^2 normalization, with the threshold chosen before every family member and arithmetic parameter.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.alpha_sq_mul_smoothWU_SWFamily_log_payment {ι : Type u_1} {κ k ℓ : ℕ} (hk : 1 ≤ k) (hℓ : 1 ≤ ℓ) (j 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 : ℝ), 1 ≤ M → 1 ≤ L → M * T i ≤ x → L ≤ x → x ^ ε ≤ T i → ∀ (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| ≤ x ^ 2 / Real.log x ^ A

Actual alpha second moment times the full W-zero-minus-U-zero difference is O(x^2 log(x)^(-A)). No large-gcd subtraction or unestimated covariance term remains, and the residue may be any varying signed integer.