! # MathlibNt.SieveTheory.BombieriVinogradov

The Bombieri--Vinogradov theorem is an analytic literature input in this development. This file deliberately states only its standard uniform average form: it does not manufacture parameter-dependent constants, and its main term is a genuine logarithmic integral rather than the proxy x / log x.

For references see Bombieri, On the large sieve (1965), Vinogradov (1965), or Halberstam--Richert, Sieve Methods, Chapter 9.

noncomputable def MathlibNt.SieveTheory.BombieriVinogradov.trueLogarithmicIntegral (x : ℝ) : ℝ

A normalized genuine logarithmic integral: 2 / log 2 + ∫ t in 2..x, 1 / log t. Thus it differs from the literal integral from 2 to x by the fixed additive constant 2 / log 2; the two normalizations are asymptotically interchangeable. This normalization is chosen so that it dominates x / log x for x ≥ 2.

Equations

• MathlibNt.SieveTheory.BombieriVinogradov.trueLogarithmicIntegral x = MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) x

def MathlibNt.SieveTheory.BombieriVinogradov.primesInAP (x q l : ℕ) : ℕ

The usual prime count through the integer endpoint x in the residue class l modulo q.

Equations

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

noncomputable def MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPError (x q l : ℕ) : ℝ

The ordinary prime-AP error centered at the genuine logarithmic integral.

Equations

• MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPError x q l = ↑(MathlibNt.SieveTheory.BombieriVinogradov.primesInAP x q l) - MathlibNt.SieveTheory.BombieriVinogradov.trueLogarithmicIntegral ↑x / ↑q.totient

noncomputable def MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError (x q : ℕ) : ℝ

The maximum standard AP error over canonical reduced residues. It is defined as 0 for the empty modulus-zero residue set; modulo 1 its unique canonical reduced residue is 0.

Equations

• MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError x q = if h : (AnalyticNumberTheory.Sieve.unitResidues q).Nonempty then (Finset.image (fun (l : ℕ) => |MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPError x q l|) (AnalyticNumberTheory.Sieve.unitResidues q)).max' ⋯ else 0

theorem MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError_zero (x : ℕ) : standardPrimeAPMaxError x 0 = 0

theorem MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError_one (x : ℕ) : standardPrimeAPMaxError x 1 = |standardPrimeAPError x 1 0|

theorem MathlibNt.SieveTheory.BombieriVinogradov.abs_standardPrimeAPError_le_max {x q l : ℕ} (hl : l ∈ AnalyticNumberTheory.Sieve.unitResidues q) : |standardPrimeAPError x q l| ≤ standardPrimeAPMaxError x q

A reduced residue is bounded by the corresponding canonical maximum.

noncomputable def MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError (x q : ℕ) : ℝ

The prefix maximum occurring in the standard Bombieri--Vinogradov theorem: first maximize over reduced residues, then over every integer endpoint y ≤ x. The finite set is always nonempty because it contains y = 0.

Equations

• MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError x q = (Finset.image (fun (y : ℕ) => MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError y q) (Finset.range (x + 1))).max' ⋯

theorem MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError_le_prefixMaxError (x q : ℕ) : standardPrimeAPMaxError x q ≤ standardPrimeAPPrefixMaxError x q

The endpoint error is one of the terms in the standard prefix maximum.

theorem MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError_nonneg (x q : ℕ) : 0 ≤ standardPrimeAPMaxError x q

The canonical maximal AP error is nonnegative at every modulus, including the explicitly defined zero endpoint.

theorem MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError_nonneg (x q : ℕ) : 0 ≤ standardPrimeAPPrefixMaxError x q

The prefix maximum is nonnegative, since every endpoint maximum is.

theorem MathlibNt.SieveTheory.BombieriVinogradov.sum_standardPrimeAPMaxError_le_prefixMaxError (x : ℕ) (S : Finset ℕ) : ∑ q ∈ S, standardPrimeAPMaxError x q ≤ ∑ q ∈ S, standardPrimeAPPrefixMaxError x q

Summing the endpoint errors over any finite modulus set is bounded by the sum of the standard prefix-maximal errors over the same set.

theorem MathlibNt.SieveTheory.BombieriVinogradov.primesInAP_modEq_N_eq (N d : ℕ) : primesInAP N d (N % d) = {p ∈ Finset.range (N + 1) | Nat.Prime p ∧ p ≡ N [MOD d]}.card

Replacing a residue by its canonical representative does not change the standard prime-AP count.

theorem MathlibNt.SieveTheory.BombieriVinogradov.div_log_le_trueLogarithmicIntegral {x : ℝ} (hx : 2 ≤ x) : x / Real.log x ≤ trueLogarithmicIntegral x

The genuine logarithmic integral dominates the historical elementary proxy.

def MathlibNt.SieveTheory.BombieriVinogradov.StandardBombieriVinogradov : Prop

Standard Bombieri--Vinogradov literature interface.

For every A > 0, a nonnegative logarithmic loss exponent B and a positive constant C work uniformly for all sufficiently large endpoints. For every modulus this uses the standard nested maxima max_{y ≤ N} max_{(l,q)=1}; in particular it is not the weaker fixed-endpoint assertion. The sum is over the genuine moduli 1 ≤ q ≤ floor(N^(1/2) / log(N)^B) with no reduction of the classical modulus range. The finite conventions at q = 0 and q = 1 are explicit above, but q = 0 is not included in this theorem.

Equations

• MathlibNt.SieveTheory.BombieriVinogradov.StandardBombieriVinogradov = ∀ (A : ℝ), 0 < A → ∃ (B : ℝ), 0 ≤ B ∧ ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → ∑ q ∈ Finset.Icc 1 (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B), MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPPrefixMaxError N q ≤ C * ↑N / Real.log ↑N ^ A

theorem MathlibNt.SieveTheory.BombieriVinogradov.endpoint_bound (hBV : StandardBombieriVinogradov) (A : ℝ) : 0 < A → ∃ (B : ℝ), 0 ≤ B ∧ ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, 2 ≤ N → ∑ q ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N B), standardPrimeAPMaxError N q ≤ C * ↑N / Real.log ↑N ^ A

The fixed-endpoint estimate used by the lower-sieve consumer is a direct finite consequence of the standard prefix-maximal theorem. This theorem keeps the producer interface standard while allowing endpoint-only consumers to use exactly the bound they need.