AnalyticNumberTheory.Sieve.BombieriVinogradov

Bombieri--Vinogradov theorem and pointwise remainder interfaces

The Bombieri--Vinogradov theorem (1965) is a central source of distribution conditions in Chen's theorem. It controls the average error in the distribution of primes in arithmetic progressions, replacing the role of the generalized Riemann hypothesis (GRH) in these mean estimates.

Classical Bombieri--Vinogradov theorem: for each fixed A > 0, there exists B = B(A) such that

Σ_{q ≤ x^(1/2) log^(-B) x} max_{y ≤ x} max_{(l,q)=1} |π(y; q, l) - li(y)/φ(q)| ≪ x / log^A x.

Here li denotes the genuine logarithmic integral. The existing API name logarithmicIntegral below instead denotes the proxy x / log x; it is not the logarithmic integral. The name is retained for compatibility.

Applications in Chen's theorem:

• The sieve distribution condition |{a ∈ A : d | a}| = ν(d)/d · X + R_d.
• Distribution level D = N^(1/2 - ε) from Bombieri--Vinogradov.
• The distribution input required for Jurkat--Richert and Selberg sieves.

This module proves fixed-parameter remainder interfaces, not the classical uniform averaged theorem.

References:

• Bombieri, E. (1965), Math. Ann. 157, 220-260
• Vinogradov, A.I. (1965), Izv. Akad. Nauk SSSR Ser. Mat. 29, 903-934
• Liu, Z. (2022), arXiv:2203.07871, Theorem 1
• Halberstam & Richert, "Sieve Methods" (1974), Ch. 9

1. Counting primes in arithmetic progressions

def AnalyticNumberTheory.Sieve.primesInAP (x q l : ℕ) : ℕ

π(x; q, l) = |{p ≤ x : p is prime, p ≡ l (mod q)}|. For a positive modulus with (l,q) = 1, Dirichlet's theorem guarantees infinitely many such primes.

Equations

• AnalyticNumberTheory.Sieve.primesInAP x q l = {p ∈ Finset.range (x + 1) | Nat.Prime p ∧ p ≡ l [MOD q]}.card

noncomputable def AnalyticNumberTheory.Sieve.logarithmicIntegral (x : ℝ) : ℝ

Compatibility proxy x / log x for the prime-counting main term.

Despite its historical name, this is not the paper's logarithmic integral li(x) = ∫₂ˣ dt / log t. The name and definition are retained to preserve the existing API; source-faithful consumers must keep the main-term model abstract.

Equations

• AnalyticNumberTheory.Sieve.logarithmicIntegral x = x / Real.log x

noncomputable def AnalyticNumberTheory.Sieve.distributionError (x q l : ℕ) : ℝ

Proxy error π(x; q, l) - (x / log x) / φ(q).

This is not definitionally the classical π(x; q, l) - li(x) / φ(q).

Equations

• AnalyticNumberTheory.Sieve.distributionError x q l = ↑(AnalyticNumberTheory.Sieve.primesInAP x q l) - AnalyticNumberTheory.Sieve.logarithmicIntegral ↑x / ↑q.totient

2. Bombieri--Vinogradov-shaped remainder interfaces

theorem AnalyticNumberTheory.Sieve.bombieri_vinogradov (A : ℝ) : 0 < A → ∀ (x : ℕ), 2 ≤ x → ∀ q ≥ 1, ∀ (y : ℕ), 2 ≤ y → y ≤ x → ∀ (l : ℕ), l.Coprime q → l < q → ∃ (C : ℝ), |distributionError y q l| ≤ C * ↑x / (Real.log ↑x ^ A * ↑q.totient)

Fixed-parameter interface for a Bombieri--Vinogradov-shaped error. The classical averaged estimate is

Σ_{q ≤ x^(1/2) log^(-B) x} max_{y ≤ x} max_{(l,q)=1} |π(y; q, l) - li(y)/φ(q)| ≪ x / log^A x.

In Chen's theorem this supplies a distribution level D = N^(1/2 - ε) for arbitrarily small ε > 0, with Σ |R_d| ≪ N / log^A N.

The genuine theorem controls an average over q with a constant uniform for all sufficiently large x. The interface below has no such sum and does not assert a uniform per-modulus bound with an extra 1/φ(q) factor; that stronger assertion is neither standard BV nor a consequence of these definitions and the available mathlib results. It only gives a multiplicative remainder constant after fixing x,q,y,l. The uniform averaged theorem requires the large sieve and Vaughan's identity.

theorem AnalyticNumberTheory.Sieve.bombieri_vinogradov_simple (A : ℝ) : 0 < A → ∀ (x : ℕ), 2 ≤ x → ∃ (B : ℝ) (D : ℝ), D = ↑x ^ (1 / 2) / Real.log ↑x ^ B ∧ ∀ (q : ℕ), ↑q ≤ D → q ≥ 1 → ∃ y ≤ x, y ≥ 2 ∧ ∀ (l : ℕ), l.Coprime q → l < q → ∃ (C : ℝ), |distributionError y q l| ≤ C * ↑x / (Real.log ↑x ^ A * ↑q.totient)

A simplified wrapper for the fixed-parameter interface, explicitly recording the scale D = x^(1/2) / log^B x. The corresponding classical target has the shape Σ_{q ≤ D} max_{(l,q)=1} |π(x; q, l) - li(x)/φ(q)| ≪ x / log^A x; this wrapper does not assert that uniform average.

3. Distribution expressions for Chen's theorem

noncomputable def AnalyticNumberTheory.Sieve.chenSieveSet (N : ℕ) : Finset ℕ

The prime indices for the Chen sieve set A = {N - p : p is prime, N^(1/10) < p < N}. The definition stores the primes p, rather than their translates N-p.

Equations

• AnalyticNumberTheory.Sieve.chenSieveSet N = {p ∈ Finset.range N | Nat.Prime p ∧ ↑N ^ (1 / 10) < ↑p ∧ ↑p < ↑N}

noncomputable def AnalyticNumberTheory.Sieve.chenX (N : ℕ) : ℝ

The prime-counting main-term approximation X = N / log N used in Chen's theorem.

Equations

• AnalyticNumberTheory.Sieve.chenX N = ↑N / Real.log ↑N

noncomputable def AnalyticNumberTheory.Sieve.chenNu (d : ℕ) : ℝ

The Goldbach-type density product ν(d) = Π_{p|d} (p-1)⁻¹ used in Chen's theorem.

Equations

• AnalyticNumberTheory.Sieve.chenNu d = ∏ p ∈ d.primeFactors, 1 / (↑p - 1)

noncomputable def AnalyticNumberTheory.Sieve.chenDistributionLevel (N : ℕ) (ε : ℝ) : ℝ

The distribution level D = N^(1/2 - ε) used in Chen's theorem.

Equations

• AnalyticNumberTheory.Sieve.chenDistributionLevel N ε = ↑N ^ (1 / 2 - ε)

theorem AnalyticNumberTheory.Sieve.chen_distribution_condition (N : ℕ) (ε : ℝ) (_hε : 0 < ε) (_hε' : ε < 1 / 2) (hN : 2 ≤ N) : ∃ (A : ℝ) (C : ℝ), ∀ (d : ℕ), ↑d ≤ chenDistributionLevel N ε → d ≥ 1 → |∑ x ∈ chenSieveSet N with d ∣ x, 1 - chenNu d / ↑d * chenX N| ≤ C * ↑N / Real.log ↑N ^ A

Fixed-N distribution remainder bound. The classical Bombieri--Vinogradov application in Chen's theorem has the form |{a ∈ A : d | a}| = ν(d)/d · X + R_d for d ≤ D = N^(1/2 - ε), with errors controlled on the scale N / log^A N for A > 0.

Here C is chosen after fixing N, so the conclusion is only a bound uniform over a finite set of moduli at that N. A genuine Bombieri--Vinogradov conclusion requires the same C for all sufficiently large N, together with the averaged error estimate.

4. Pan-shaped remainder interface

theorem AnalyticNumberTheory.Sieve.pan_mean_value_theorem (A : ℝ) : 0 < A → ∀ (x : ℕ), 2 ≤ x → ∀ q ≥ 1, ∀ (y : ℕ), 2 ≤ y → y ≤ x → ∀ (l : ℕ), l.Coprime q → l < q → ∃ (C : ℝ), ↑(ArithmeticFunction.moebius q) ^ 2 * 3 ^ q.primeFactors.card * |∑ a ∈ Finset.range x, if a.Coprime q then distributionError y q l else 0| ≤ C * ↑x / Real.log ↑x ^ A

Fixed-parameter remainder interface of Pan type. The classical weighted target is

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

where f(a) is the characteristic function used in Chen's theorem and Δ(y; a, q, l) = π(y; a, q, l) - li(y/a)/φ(q). Pan's theorem is a weighted extension of Bombieri--Vinogradov, used to estimate the remainder R in the upper bound for Ω.

In the current definition, distributionError y q l, summed over range x, does not depend on a, so it is not the weighted distribution error in the literature. The conclusion below only provides a multiplicative remainder constant for fixed parameters; it does not place C before all x,q,y,l. The genuine Pan theorem requires an error depending on a and a single constant uniform for all sufficiently large x.

5. Parameter choices in Chen's theorem

noncomputable def AnalyticNumberTheory.Sieve.chenSieveLevel (N : ℕ) : ℝ

The Chen sifting level z = N^(1/10).

Equations

• AnalyticNumberTheory.Sieve.chenSieveLevel N = ↑N ^ (1 / 10)

noncomputable def AnalyticNumberTheory.Sieve.chenSwitchLevel (N : ℕ) : ℝ

The Chen switching parameter y = N^(1/3).

Equations

• AnalyticNumberTheory.Sieve.chenSwitchLevel N = ↑N ^ (1 / 3)

noncomputable def AnalyticNumberTheory.Sieve.chenSelbergLevel (N : ℕ) (ε : ℝ) : ℝ

The Chen Selberg sifting level z' = N^(1/4 - ε/2).

Equations

• AnalyticNumberTheory.Sieve.chenSelbergLevel N ε = ↑N ^ (1 / 4 - ε / 2)

noncomputable def AnalyticNumberTheory.Sieve.chenSieveRatio (_N : ℕ) (ε : ℝ) : ℝ

Sieve ratio s = log(D)/log(z) = (1/2 - ε)/(1/10) = 5 - 10ε.

Equations

• AnalyticNumberTheory.Sieve.chenSieveRatio _N ε = (1 / 2 - ε) / (1 / 10)

theorem AnalyticNumberTheory.Sieve.chenSieveRatio_approx (ε : ℝ) (hε : 0 < ε) (hε' : ε < 1 / 100) : 4.9 < chenSieveRatio 0 ε ∧ chenSieveRatio 0 ε < 5

For sufficiently small positive ε, the sieve ratio is close to 5.

6. Mathematical scope