AnalyticNumberTheory.Sieve.WeightedPan

Weighted Pan--Bombieri--Vinogradov input

The upper bound for Ω in Chen's theorem, and more general Goldbach-type sieves, requires a weighted average distribution condition, not a uniform bound for each modulus: for each A > 0, a uniform constant C gives Σ_{d|P} 3^{ω(d)}·|Δ(d)| ≤ C·x/log^A x. Here Δ(d) is the difference between the congruence count and ν(d)·x/log x. The weight counts pairs (d₁,d₂) with [d₁,d₂]=d in the Selberg expansion (lcmPairCount).

This module supplies:

1. Finite weight identities: for squarefree d, 3^{ω(d)} counts lcm pairs; hence Σ_{d|Q}3^{ω(d)}f(d) = Σ_{d₁|Q}Σ_{d₂|Q}f([d₁,d₂]) for squarefree Q (lcmPairWeightedSum).
2. Sieve application interface: WeightedPanCondition for a family S N : BoundingSieve and scale x N. In the Chen specialization, x N = N, S N = correctedChenBoundingSieve N, and w d = 3^{ω(d)}; |S.rem d| is the absolute congruence-count error |#{p∈support : p≡N [MOD d]} − ν(d)·N/log N|.
3. Weighted mean-value target: PanMeanValueUniform has the classical logarithmic-saving shape Σ_{q≤(x X)^{1/2}/log^B(x X)} μ²(q)·3^{ω(q)} ·max_{y≤x X} max_{0<l<q,(l,q)=1} |Σ_{a≤X,(a,q)=1} f(a)·Δ(y;a,q,l)| ≤ C·x X/log^A(x X), with constants preceding all sufficiently large X.

The large sieve and Vaughan's identity are analytic ingredients for the classical Pan theorem (Pan 1963; Halberstam--Richert 1974 Ch. 10; Liu 2022 §III). This module fixes definitions and proves finite bridges, not an unconditional uniform mean-value theorem. The implemented main term uses the x/log x proxy; connecting it to a classical logarithmic-integral formulation and to sieve remainders requires additional main-term and support analysis. The coarse polylogarithmic proposition is kept separate.

References:

• Pan, C.D. (1963), Sci. Sinica 12, 465-473
• Bombieri, E. (1965), Math. Ann. 157, 220-260
• Vinogradov, A.I. (1965), Izv. Akad. Nauk SSSR 29, 903-934
• Halberstam & Richert, "Sieve Methods" (1974), Ch. 10
• Liu, Z. (2022), arXiv:2203.07871

1. Origin of the weight: 3^{ω(d)} counts lcm pairs

theorem AnalyticNumberTheory.Sieve.lcmPairCount (d : ℕ) (hsq : Squarefree d) : {x ∈ d.divisors ×ˢ d.divisors | x.1.lcm x.2 = d}.card = 3 ^ d.primeFactors.card

For squarefree d, exactly 3^{ω(d)} divisor pairs (d₁,d₂) satisfy lcm d₁ d₂ = d. Each prime factor has three exponent choices: (0,1), (1,0), and (1,1). This is the exact source of the Selberg upper-sieve weight 3^{ω(d)}.

theorem AnalyticNumberTheory.Sieve.lcmPairWeightedSum (Q : ℕ) (hQ : Squarefree Q) (f : ℕ → ℝ) : ∑ d ∈ Q.divisors, 3 ^ d.primeFactors.card * f d = ∑ d₁ ∈ Q.divisors, ∑ d₂ ∈ Q.divisors, f (d₁.lcm d₂)

Grouping the Selberg double sum: for squarefree Q, Σ_{d|Q} 3^{ω(d)}·f(d) = Σ_{d₁|Q} Σ_{d₂|Q} f([d₁,d₂]). The weight counts pairs with lcm d (lcmPairCount). This exact finite identity turns the lcm double sum into the single weighted sum used by the Pan input.

1b. Pan weight decomposition: 3^{ω(q)} = Σ_{d|q} 2^{ω(d)}

theorem AnalyticNumberTheory.Sieve.threeOmega_eq_sum_twoOmega_divisors {q : ℕ} (hq : Squarefree q) : 3 ^ q.primeFactors.card = ∑ d ∈ q.divisors, 2 ^ d.primeFactors.card

Pan weight decomposition (Pan 1963; see also the weighted form of Halberstam--Richert 1974 Lemma 10.3): for squarefree q, 3^{ω(q)} = Σ_{d|q} 2^{ω(d)} = Σ_{d|q} τ(d), since 2^{ω(d)} = τ(d) for squarefree d. The three choices for each prime are regrouped by the divisor d and its two inclusion choices. This divisor expansion is the mechanism for handling the 3^{ω(q)} weight in the outer modulus sum of the weighted Pan argument.

theorem AnalyticNumberTheory.Sieve.threeOmegaWeightedSum_packaging (Q : ℕ) (hQ : Squarefree Q) (f : ℕ → ℝ) : ∑ q ∈ Q.divisors, 3 ^ q.primeFactors.card * f q = ∑ d ∈ Q.divisors, 2 ^ d.primeFactors.card * ∑ m ∈ (Q / d).divisors, f (d * m)

Regrouping Pan weights: for squarefree Q, Σ_{q|Q}3^{ω(q)}f(q) = Σ_{d|Q}2^{ω(d)}·Σ_{m|Q/d}f(d·m). Combine 3^{ω(q)} = Σ_{d|q}2^{ω(d)} with the divisibility-indexed bijection (q,d) ↔ (d,m=q/d). This replaces the 3^{ω(q)}-weighted modulus sum by a 2^{ω(d)}-weighted double sum, as in Pan's classical enlargement of the modulus sum (1963).

2. Uniform weighted distribution interface for sieve applications

noncomputable def AnalyticNumberTheory.Sieve.weightedPanRemainder (S : BoundingSieve) (w : ℕ → ℝ) : ℝ

Weighted remainder sum over sieve-product divisors: Σ_{d|P} w(d)·|rem d|, where rem d = multSum d − ν(d)·totalMass is the BoundingSieve distribution remainder.

Equations

• AnalyticNumberTheory.Sieve.weightedPanRemainder S w = ∑ d ∈ S.prodPrimes.divisors, w d * |BoundingSieve.rem d|

theorem AnalyticNumberTheory.Sieve.weightedPanRemainder_eq_lcmDoubleSum (S : BoundingSieve) : (weightedPanRemainder S fun (d : ℕ) => 3 ^ d.primeFactors.card) = ∑ d₁ ∈ S.prodPrimes.divisors, ∑ d₂ ∈ S.prodPrimes.divisors, |BoundingSieve.rem (d₁.lcm d₂)|

The 3^{ω(d)}-weighted remainder is exactly the lcm double sum Σ_{d₁,d₂}|rem [d₁,d₂]| in the Selberg expansion.

theorem AnalyticNumberTheory.Sieve.errSum_le_threeOmegaWeightedPanRemainder {S : BoundingSieve} : (BoundingSieve.errSum fun (x : ℕ) => 1) ≤ weightedPanRemainder S fun (d : ℕ) => 3 ^ d.primeFactors.card

The counting-sieve error with coefficient sequence 1 is bounded by the 3^{ω(d)}-weighted remainder sum, generalizing correctedChenErrSum_le_panWeighted.

theorem AnalyticNumberTheory.Sieve.errSum_lambdaSquared_le_threeOmegaWeightedPanRemainder {S : BoundingSieve} {w : ℕ → ℝ} (hw : ∀ (d : ℕ), |w d| ≤ 1) : BoundingSieve.errSum (BoundingSieve.lambdaSquared w) ≤ weightedPanRemainder S fun (d : ℕ) => 3 ^ d.primeFactors.card

Grouping the Λ²-weight remainder: if ∀ d, |w d| ≤ 1, then |Λ²w(d)| ≤ 3^{ω(d)} for squarefree d, by the lcm-pair count lcmPairCount. Therefore errSum(Λ²w) ≤ Σ_{d|P}3^{ω(d)}·|rem d| = weightedPanRemainder S 3^ω. This is the finite Selberg remainder Σ 3^{ω(d)}|Δ(d)|, connecting a weighted Pan input to selberg_upper_bound_sieveProduct in the Chen upper bound for Ω.

def AnalyticNumberTheory.Sieve.WeightedPanCondition (x : ℕ → ℝ) (S : ℕ → BoundingSieve) (w : ℕ → ℝ) : Prop

Uniform weighted Pan distribution condition: for each A > 0, there is a uniform C > 0 such that for every even N ≥ 1000, Σ_{d|P(N)} w(d)·|rem(N,d)| ≤ C·x(N)/log^A x(N).

For x N = N, S N = correctedChenBoundingSieve N, and w d = 3^{ω(d)}, the absolute remainder is |#{p∈support : p≡N [MOD d]} − ν(d)·N/log N|, the form in CorrectedChenDistributionCondition. Once this input holds, errSum_le_threeOmegaWeightedPanRemainder gives errSum = O(N/log^A N). The constant precedes ∀ N; the threshold in this API is the fixed value 1000.

Equations

• AnalyticNumberTheory.Sieve.WeightedPanCondition x S w = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∀ (N : ℕ), 1000 ≤ N → Even N → AnalyticNumberTheory.Sieve.weightedPanRemainder (S N) w ≤ C * x N / Real.log (x N) ^ A

def AnalyticNumberTheory.Sieve.ThreeOmegaWeightedPanCondition (x : ℕ → ℝ) (S : ℕ → BoundingSieve) : Prop

The 3^{ω(d)}-weighted specialization needed in Chen's theorem.

Equations

• AnalyticNumberTheory.Sieve.ThreeOmegaWeightedPanCondition x S = AnalyticNumberTheory.Sieve.WeightedPanCondition x S fun (d : ℕ) => 3 ^ d.primeFactors.card

3. Weighted Pan mean-value target

def AnalyticNumberTheory.Sieve.primesInAPBelow (y a q l : ℕ) : ℕ

π(y;a,q,l): count primes p with a·p ≤ y and a·p ≡ l [MOD q], as in Liu 2022 §II for positive a. The definition explicitly searches p ≤ y, including at a = 0. The congruence is on the product a·p, not on p; this is the scaled AP prime count in the error for the Ω bound.

Equations

• AnalyticNumberTheory.Sieve.primesInAPBelow y a q l = {p ∈ Finset.range (y + 1) | Nat.Prime p ∧ a * p ≤ y ∧ a * p ≡ l [MOD q]}.card

noncomputable def AnalyticNumberTheory.Sieve.panDistributionError (y a q l : ℕ) : ℝ

The scaled proxy error π(y; a, q, l) - logarithmicIntegral(y/a)/φ(q).

Here logarithmicIntegral is the x / log x proxy, not the paper's true logarithmic integral. Source-facing Liu interfaces should parameterize the main-term function instead of identifying the two.

Equations

• AnalyticNumberTheory.Sieve.panDistributionError y a q l = ↑(AnalyticNumberTheory.Sieve.primesInAPBelow y a q l) - AnalyticNumberTheory.Sieve.logarithmicIntegral (↑y / ↑a) / ↑q.totient

noncomputable def AnalyticNumberTheory.Sieve.panDistributionSum (y X q l : ℕ) (f : ℕ → ℝ) : ℝ

Weighted distribution-error sum modulo q: Σ_{(a,q)=1, a≤X} f(a)·Δ(y;a,q,l). This is a signed sum, before taking absolute values. The restriction (a,q)=1 is essential to Liu §IV's correction.

Equations

• AnalyticNumberTheory.Sieve.panDistributionSum y X q l f = ∑ a ∈ Finset.range (X + 1), if a.Coprime q then f a * AnalyticNumberTheory.Sieve.panDistributionError y a q l else 0

noncomputable def AnalyticNumberTheory.Sieve.panDistributionFullSum (y X q l : ℕ) (f : ℕ → ℝ) : ℝ

The unrestricted inner sum occurring before Liu's coprime/non-coprime partition of the paper remainder R.

Equations

• AnalyticNumberTheory.Sieve.panDistributionFullSum y X q l f = ∑ a ∈ Finset.range (X + 1), f a * AnalyticNumberTheory.Sieve.panDistributionError y a q l

noncomputable def AnalyticNumberTheory.Sieve.panDistributionNoncoprimeSum (y X q l : ℕ) (f : ℕ → ℝ) : ℝ

The signed non-coprime part removed from panDistributionSum.

Equations

• AnalyticNumberTheory.Sieve.panDistributionNoncoprimeSum y X q l f = ∑ a ∈ Finset.range (X + 1), if ¬a.Coprime q then f a * AnalyticNumberTheory.Sieve.panDistributionError y a q l else 0

noncomputable def AnalyticNumberTheory.Sieve.panDistributionNoncoprimeMajorant (y X q l : ℕ) (f : ℕ → ℝ) : ℝ

The termwise absolute majorant of the non-coprime part. This is the finite inner sum used in Liu's R₁, before the outer modulus weights are applied.

Equations

• AnalyticNumberTheory.Sieve.panDistributionNoncoprimeMajorant y X q l f = ∑ a ∈ Finset.range (X + 1), if ¬a.Coprime q then |f a| * |AnalyticNumberTheory.Sieve.panDistributionError y a q l| else 0

theorem AnalyticNumberTheory.Sieve.panDistributionFullSum_eq_coprime_add_noncoprime (y X q l : ℕ) (f : ℕ → ℝ) : panDistributionFullSum y X q l f = panDistributionSum y X q l f + panDistributionNoncoprimeSum y X q l f

Exact finite partition of the unrestricted paper sum into its coprime Pan part and its signed non-coprime part.

theorem AnalyticNumberTheory.Sieve.abs_panDistributionNoncoprimeSum_le (y X q l : ℕ) (f : ℕ → ℝ) : |panDistributionNoncoprimeSum y X q l f| ≤ panDistributionNoncoprimeMajorant y X q l f

The signed non-coprime sum is bounded by Liu's termwise R₁ majorant.

theorem AnalyticNumberTheory.Sieve.abs_panDistributionFullSum_le_coprime_add_noncoprime (y X q l : ℕ) (f : ℕ → ℝ) : |panDistributionFullSum y X q l f| ≤ |panDistributionSum y X q l f| + panDistributionNoncoprimeMajorant y X q l f

Liu's finite R = R_coprime + R_noncoprime triangle bound. The first term is the source-faithful Pan sum; the second is the still-separate R₁ majorant.

def AnalyticNumberTheory.Sieve.unitResidues (q : ℕ) : Finset ℕ

Canonical representatives of the reduced residue classes modulo q. For q = 1 this is the singleton {0}; for q = 0 it is empty.

Equations

• AnalyticNumberTheory.Sieve.unitResidues q = {l ∈ Finset.range q | l.Coprime q}

@[simp]

theorem AnalyticNumberTheory.Sieve.unitResidues_zero : unitResidues 0 = ∅

@[simp]

theorem AnalyticNumberTheory.Sieve.unitResidues_one : unitResidues 1 = {0}

theorem AnalyticNumberTheory.Sieve.unitResidues_eq_Icc_filter {q : ℕ} (hq : 1 < q) : unitResidues q = {l ∈ Finset.Icc 1 (q - 1) | l.Coprime q}

For a nontrivial modulus, the canonical representatives agree with the traditional interval 1 ≤ l ≤ q - 1.

noncomputable def AnalyticNumberTheory.Sieve.panMaxL (y X q : ℕ) (f : ℕ → ℝ) : ℝ

max_{0≤l<q,(l,q)=1} |panDistributionSum y X q l f|, with the unique class modulo 1 represented by 0; the empty q = 0 maximum is 0.

Equations

• AnalyticNumberTheory.Sieve.panMaxL y X q f = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => |AnalyticNumberTheory.Sieve.panDistributionSum y X q l f|) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

@[simp]

theorem AnalyticNumberTheory.Sieve.panMaxL_zero (y X : ℕ) (f : ℕ → ℝ) : panMaxL y X 0 f = 0

@[simp]

theorem AnalyticNumberTheory.Sieve.panMaxL_one (y X : ℕ) (f : ℕ → ℝ) : panMaxL y X 1 f = |panDistributionSum y X 1 0 f|

noncomputable def AnalyticNumberTheory.Sieve.panMaxY (X q x : ℕ) (f : ℕ → ℝ) : ℝ

max_{y≤x} panMaxL y X q f: uniform maximum over the truncation parameter y, as in Liu Theorem 2.

Equations

• AnalyticNumberTheory.Sieve.panMaxY X q x f = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.Sieve.panMaxL y X q f) (Finset.range (x + 1))).max' ⋯

@[simp]

theorem AnalyticNumberTheory.Sieve.panMaxY_zero (X x : ℕ) (f : ℕ → ℝ) : panMaxY X 0 x f = 0

theorem AnalyticNumberTheory.Sieve.panMaxY_one (X x : ℕ) (f : ℕ → ℝ) : panMaxY X 1 x f = (Finset.image (fun (y : ℕ) => |panDistributionSum y X 1 0 f|) (Finset.range (x + 1))).max' ⋯

def AnalyticNumberTheory.Sieve.PanMeanValueUniformCrude (x f : ℕ → ℝ) : Prop

Coarse pure-li bound: the polylogarithmic result of separating the positive main term and taking its absolute value in the coarse Vaughan chain. It is not Liu 2022 Theorem 2 and cannot supply WeightedPanCondition. This separate proposition records exactly the scope of the coarse reductions.

Equations

• AnalyticNumberTheory.Sieve.PanMeanValueUniformCrude x f = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panMaxY X q ⌊x X⌋₊ f ≤ C * x X * Real.log (x X) ^ (A + 7)

def AnalyticNumberTheory.Sieve.PanMeanValueUniform (x f : ℕ → ℝ) : Prop

Weighted Pan mean-value target, with the quantifier and signed-sum structure of Liu 2022 Theorem 2: for each A > 0, there are C > 0, B, and x₀ such that for all X ≥ x₀,

Σ_{q ≤ (x X)^{1/2}/log^B(x X)} μ²(q)·3^{ω(q)}· max_{y ≤ x X} max_{0<l<q,(l,q)=1} |Σ_{(a,q)=1, a≤X} f(a)·Δ(y;a,q,l)| ≤ C·x X/log^A(x X).

Here Δ(y;a,q,l) = π(y;a,q,l) − li(y/a)/φ(q), with the implemented li name denoting the x/log x proxy. Three structural features are essential (see PAN_PROOF_ATLAS.md): the inner coprimality restriction, the maximum over y, and the absolute value around the whole signed sum, not Σ f·|Δ|. Dropping coprimality fails for the Chen weights: Liu §IV's R₁ correction depends on the specific weight and sieve product and is handled in the Chen application.

The inverse logarithm bounds the signed distribution error, not a pure absolute-li block. The coarse split gives only PanMeanValueUniformCrude. A classical proof retains li and the Vaughan middle/small terms inside one absolute value, while the nondecaying Selberg main term remains in the Chen main-term estimate; this is Liu §III's M = M₁ + R separation.

This proposition is an analytic input, not an unconditional theorem proved here. The classical error estimate for Ω uses the large sieve and Vaughan's identity (Pan 1963; Halberstam--Richert 1974 Ch. 10; Liu 2022 §III). Connecting it to WeightedPanCondition additionally requires support truncation and main-term comparison, including the classical relation li(x) = x/log x + O(x/log²x) with the genuine logarithmic integral.

Equations

• AnalyticNumberTheory.Sieve.PanMeanValueUniform x f = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ) (x₀ : ℕ), ∀ (X : ℕ), x₀ ≤ X → ∑ q ∈ Finset.range (⌊x X ^ (1 / 2) / Real.log (x X) ^ B⌋₊ + 1), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * AnalyticNumberTheory.Sieve.panMaxY X q ⌊x X⌋₊ f ≤ C * x X / Real.log (x X) ^ A

From the Pan expression to sieve remainders

At a = 1, primesInAPBelow y a q l is the ordinary count #{p≤y : p is prime, p≡l [MOD q]}. This identifies the source of the sieve remainder #{p∈support : p≡N [MOD d]}. Further comparison hypotheses are needed to bound the sieve's weighted remainder sum by the 3^{ω(q)}-weighted panMaxY sum.

WeightedPanCondition requires C·xN/log^A(xN) for every A > 0; the switching sieve and error absorption need arbitrarily large logarithmic savings. PanMeanValueUniformCrude, with right side C·xX·(log xX)^{A+7}, cannot meet that requirement. PanMeanValueUniform retains the inverse-log target and is assembled only under analytic inputs such as PanSourceFaithfulSignedMainBound.

The generic absolute-value chain under |f| ≤ 1 cannot provide the saving. The inner pure-main-term sum has a refined y·(1+log log y) shape in suitable ranges, or the coarse bound (y/log 2)·(1+log X); multiplying by the q-factor log⁶ does not produce inverse-log decay. Even retaining coprimality, the choice f = 1 leaves a pure-main-term contribution of the indicated (y/log y)·log X size. The classical application needs the specific Chen weights and control of their harmonic sum Σ f(a)/a, together with the sieve main term of shape x/log x·∏(1-ν(p)/p) in the unnormalized density convention. The saving is a difference estimate |main term − sieve main term| ≪ x/log^A x. These weight and main-term requirements belong to the Chen application and its analytic bridge, not to the a = 1 identities below; see PAN_PROOF_ATLAS.md.

theorem AnalyticNumberTheory.Sieve.primesInAPBelow_one (y q l : ℕ) : primesInAPBelow y 1 q l = {p ∈ Finset.range (y + 1) | Nat.Prime p ∧ p ≡ l [MOD q]}.card

At a = 1, the scaled count is the ordinary AP prime count.

theorem AnalyticNumberTheory.Sieve.primesInAPBelow_one_eq_primesInAP (y q l : ℕ) : primesInAPBelow y 1 q l = primesInAP y q l

At a = 1, the scaled count equals primesInAP, the ordinary AP count in the BV interface.

theorem AnalyticNumberTheory.Sieve.panDistributionError_one (y q l : ℕ) : panDistributionError y 1 q l = ↑{p ∈ Finset.range (y + 1) | Nat.Prime p ∧ p ≡ l [MOD q]}.card - logarithmicIntegral ↑y / ↑q.totient

At a = 1, the distribution error is π(y;q,l) − li(y)/φ(q), the ordinary AP prime error for the implemented main-term proxy.