Finite beta covariance in the actual W and U zero modes

The algebra of Fouvry (1984), p. 242, (9.2) and the following unnumbered identity, for the full unpruned zero mode. No spectral estimate or use of (9.1) is involved. All beta and modulus coefficients remain signed.

The discrepancy estimates below are conditional on independent beta arithmetic-progression estimates; they do not prove a Siegel--Walfisz estimate or the final Fouvry distribution bound.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaReducedResidues (δ : ℕ) : Finset ℕ

Canonical representatives of the reduced residue classes, including the representative zero when the modulus is one.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaReducedResidues δ = {b ∈ Finset.range δ | b.Coprime δ}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaReducedResidues_card (δ : ℕ) : (betaReducedResidues δ).card = δ.totient

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaResidueMass (N : Finset ℕ) (β : ℕ → ℝ) (q δ b : ℕ) : ℝ

The original coprime sieve is retained, even when the progression modulus is only a divisor of the sieving modulus.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaResidueMass N β q δ b = ∑ n ∈ N, if n.Coprime q ∧ n ≡ b [MOD δ] then β n else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_betaResidueMass (N : Finset ℕ) (β : ℕ → ℝ) {q δ : ℕ} (hδ : 0 < δ) (hdq : δ ∣ q) : ∑ b ∈ betaReducedResidues δ, betaResidueMass N β q δ b = coprimeMass N β q

Partition of the actual signed coprime mass over reduced classes. This applies to either modulus in a pair since their gcd divides both.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.compatible_beta_sum_eq_residue_products (N : Finset ℕ) (β : ℕ → ℝ) {q r : ℕ} (hq : 0 < q) : (∑ n₁ ∈ N, ∑ n₂ ∈ N, if WCompatible q r n₁ n₂ then β n₁ * β n₂ else 0) = ∑ b ∈ betaReducedResidues (q.gcd r), betaResidueMass N β q (q.gcd r) b * betaResidueMass N β r (q.gcd r) b

The compatibility sum in smoothWMain is precisely a sum of products of beta masses in the same reduced residue class.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCovariance (N : Finset ℕ) (β : ℕ → ℝ) (q r : ℕ) : ℝ

Centered beta covariance on the reduced classes modulo the gcd.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCovariance N β q r = ∑ b ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaReducedResidues (q.gcd r), (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaResidueMass N β q (q.gcd r) b - MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass N β q / ↑(q.gcd r).totient) * (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaResidueMass N β r (q.gcd r) b - MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass N β r / ↑(q.gcd r).totient)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.beta_covariance_identity (N : Finset ℕ) (β : ℕ → ℝ) {q r : ℕ} (hq : 0 < q) : ∑ b ∈ betaReducedResidues (q.gcd r), betaResidueMass N β q (q.gcd r) b * betaResidueMass N β r (q.gcd r) b - coprimeMass N β q * coprimeMass N β r / ↑(q.gcd r).totient = betaCovariance N β q r

F84 p. 242, the unnumbered identity following (9.2). Both centering identities are proved from the actual coprime masses, not assumed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.totient_pair_density_eq_lcm {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) : ↑(q * r).totient / (↑q.totient * ↑r.totient * ↑(q * r)) = 1 / (↑(q.lcm r) * ↑(q.gcd r).totient)

The totient and lcm identity responsible for the U coefficient in (9.2). It holds for arbitrary nonzero moduli, not only coprime moduli.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.uModulusCoefficient_zeroMode_eq (N : Finset ℕ) (β c : ℕ → ℝ) {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) : uModulusCoefficient N β c q r * (↑(q * r).totient / ↑(q * r)) = c q * c r / (↑(q.lcm r) * ↑(q.gcd r).totient) * coprimeMass N β q * coprimeMass N β r

The U summand has exactly the lcm-times-totient denominator, with the original signed modulus coefficients and signed beta totals.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothUMain_eq_residue_means (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hQ : ∀ q ∈ Q, q ≠ 0) : smoothUMain M N Q β c a = M * dyadicCutoffMass * ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, c q * c r / ↑(q.lcm r) * (coprimeMass N β q * coprimeMass N β r / ↑(q.gcd r).totient)

The full signed U zero mode in the normalization of the W zero mode.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWMain_sub_smoothUMain_eq_betaCovariance (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hQ : ∀ q ∈ Q, q ≠ 0) : smoothWMain M N Q β c a - smoothUMain M N Q β c a = M * dyadicCutoffMass * ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, c q * c r / ↑(q.lcm r) * betaCovariance N β q r

Actual W-minus-U zero-mode cancellation, the independent finite algebra of F84 (9.2), without assuming that this difference is small. No positivity is imposed on the scale or either coefficient sequence.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCovariance_abs_le (N : Finset ℕ) (β : ℕ → ℝ) (q r : ℕ) (Eq Er : ℝ) (hEq : ∀ b ∈ betaReducedResidues (q.gcd r), |betaResidueMass N β q (q.gcd r) b - coprimeMass N β q / ↑(q.gcd r).totient| ≤ Eq) (hEr : ∀ b ∈ betaReducedResidues (q.gcd r), |betaResidueMass N β r (q.gcd r) b - coprimeMass N β r / ↑(q.gcd r).totient| ≤ Er) : |betaCovariance N β q r| ≤ ↑(q.gcd r).totient * Eq * Er

Conditional estimate from independent pointwise beta-AP discrepancies. The error bounds need not be assumed nonnegative separately.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCoprimeAPDiscrepancy (N : Finset ℕ) (β : ℕ → ℝ) (d h b : ℕ) : ℝ

The beta-AP discrepancy with the additional, exact coprime sieve. This is an analytic input to a Siegel--Walfisz hypothesis, not a claim that arbitrary beta coefficients satisfy one.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCoprimeAPDiscrepancy N β d h b = (∑ n ∈ N, if n.Coprime h ∧ n ≡ b [MOD d] then β n else 0) - MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimeMass N β (d * h) / ↑d.totient

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaResidueMass_eq_quotientSieve (N : Finset ℕ) (β : ℕ → ℝ) {q δ b : ℕ} (hdq : δ ∣ q) (hb : b.Coprime δ) : betaResidueMass N β q δ b = ∑ n ∈ N, if n.Coprime (q / δ) ∧ n ≡ b [MOD δ] then β n else 0

On a reduced class, the sieve by q is exactly the sieve by q / δ. No prime-support assumption on beta is made.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaResidueMass_centered_eq_coprimeAPDiscrepancy (N : Finset ℕ) (β : ℕ → ℝ) {q δ b : ℕ} (hdq : δ ∣ q) (hb : b.Coprime δ) : betaResidueMass N β q δ b - coprimeMass N β q / ↑δ.totient = betaCoprimeAPDiscrepancy N β δ (q / δ) b

Bridge to the F87 coprime-sieved beta-SW input. The total mass is at δ * (q / δ) = q, rather than an unsieved or prime-only total.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaCovariance_abs_le_of_coprimeAP (N : Finset ℕ) (β : ℕ → ℝ) (q r : ℕ) (Eq Er : ℝ) (hEq : ∀ b ∈ betaReducedResidues (q.gcd r), |betaCoprimeAPDiscrepancy N β (q.gcd r) (q / q.gcd r) b| ≤ Eq) (hEr : ∀ b ∈ betaReducedResidues (q.gcd r), |betaCoprimeAPDiscrepancy N β (q.gcd r) (r / q.gcd r) b| ≤ Er) : |betaCovariance N β q r| ≤ ↑(q.gcd r).totient * Eq * Er

Direct conditional covariance bound from the two independently supplied coprime-sieved AP bounds, in the normalization of the F87 beta-SW input.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWMain_sub_smoothUMain_abs_le_of_coprimeAP (M : ℝ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (hQ : ∀ q ∈ Q, q ≠ 0) (E : ℕ → ℕ → ℝ) (hE : ∀ q ∈ Q, ∀ (d : ℕ), d ∣ q → 0 < d → ∀ b ∈ betaReducedResidues d, |betaCoprimeAPDiscrepancy N β d (q / d) b| ≤ E q d) : |smoothWMain M N Q β c a - smoothUMain M N Q β c a| ≤ |M * dyadicCutoffMass| * ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, |c q * c r / ↑(q.lcm r)| * (↑(q.gcd r).totient * E q (q.gcd r) * E r (q.gcd r))

A conditional aggregate consequence of independent beta-AP input at each positive divisor of each sieving modulus. This is not a logarithmic saving: no estimate for the resulting modulus sum is asserted.