Small gcd contribution to the actual W-minus-U zero mode

The beta input is an independent coprime-sieved AP discrepancy estimate. An L-infinity times L-one covariance bound avoids a factor of the gcd. Elementary reciprocal divisor means then evaluate the entire small-gcd modulus sum. The complementary large-gcd contribution is left explicit.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaResidueMass_abs_le (N : Finset ℕ) (β : ℕ → ℝ) (q δ b : ℕ) : |betaResidueMass N β q δ b| ≤ betaResidueMass N (fun (n : ℕ) => |β n|) q δ b

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_betaResidueMass_centered_le (N : Finset ℕ) (β : ℕ → ℝ) {q δ : ℕ} (hδ : 0 < δ) (hdq : δ ∣ q) : ∑ b ∈ betaReducedResidues δ, |betaResidueMass N β q δ b - coprimeMass N β q / ↑δ.totient| ≤ 2 * ∑ n ∈ N, |β n|

Centering on reduced classes costs at most twice the original L-one mass. The partition uses the actual coprime sieve by q.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCovariance_abs_le_coprimeAP_lone (N : Finset ℕ) (β : ℕ → ℝ) {q r : ℕ} (hq : 0 < q) {E : ℝ} (hE : 0 ≤ E) (hAP : ∀ b ∈ betaReducedResidues (q.gcd r), |betaCoprimeAPDiscrepancy N β (q.gcd r) (q / q.gcd r) b| ≤ E) : |betaCovariance N β q r| ≤ 2 * E * ∑ n ∈ N, |β n|

Only one independent AP bound is needed, with no totient/gcd factor.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_div_le_succ (κ : ℕ) {q δ : ℕ} (hq : q ≠ 0) (hdq : δ ∣ q) : (fouvryTau κ) (q / δ) ≤ (fouvryTau (κ + 1)) q

A single term of the divisor convolution suffices; no monotonicity of prime-power divisor coefficients is required.

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

The signed small-gcd part in the exact normalization of W zero minus U zero.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWUSmallDelta M D 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, if ↑(q.gcd r) ≤ D then c q * c r / ↑(q.lcm r) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCovariance N β q r else 0

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

The signed large-gcd remainder. No estimate for this term is asserted.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWULargeDelta M D 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, if D < ↑(q.gcd r) then c q * c r / ↑(q.lcm r) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCovariance N β q r else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWMain_sub_smoothUMain_eq_small_add_large (M D : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hQ : ∀ q ∈ Q, q ≠ 0) : smoothWMain M N Q β c a - smoothUMain M N Q β c a = smoothWUSmallDelta M D N Q β c a + smoothWULargeDelta M D N Q β c a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_reduced_abs_mul_tau_div_le (j κ : ℕ) {L : ℝ} (hL : 1 ≤ L) (Q : Finset ℕ) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) : ∑ q ∈ reducedModuli Q a, |c q| * ↑((fouvryTau κ) q) / ↑q ≤ (1 + Real.log L) ^ (j * κ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_reduced_abs_div_le (j : ℕ) {L : ℝ} (hL : 1 ≤ L) (Q : Finset ℕ) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) : ∑ q ∈ reducedModuli Q a, |c q| / ↑q ≤ (1 + Real.log L) ^ j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWUSmallDelta_abs_le {k : ℕ} (hk : 1 ≤ k) (j κ : ℕ) {T L D E : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (hD : 0 ≤ D) (hE : 0 ≤ E) (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 : ℤ) (hAP : ∀ q ∈ Q, ∀ (δ : ℕ), δ ∣ q → 0 < δ → ↑δ ≤ D → ∀ b ∈ betaReducedResidues δ, |betaCoprimeAPDiscrepancy N β δ (q / δ) b| ≤ E * ↑((fouvryTau κ) (q / δ))) : |smoothWUSmallDelta M D N Q β c a| ≤ 2 * |M * dyadicCutoffMass| * E * (T * (1 + Real.log T) ^ (k - 1)) * D * (1 + Real.log L) ^ (j * (κ + 2))

The small-gcd double modulus sum is completely evaluated. Beta order k and coprime-sieve order κ are independent, and all weights stay signed. There is no AP hypothesis at large gcd and no assumption on the target error.