Documentation

MathlibNt.SieveTheory.Distribution.BombieriVinogradov

! # 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.

source
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
Instances For
    source
    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
    Instances For
      source
      noncomputable def MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPError (x q l : ℕ) :
      ℝ

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

      Equations
      Instances For
        source
        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
        Instances For
          source
          theorem MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError_zero (x : ℕ) :
          standardPrimeAPMaxError x 0 = 0
          source
          theorem MathlibNt.SieveTheory.BombieriVinogradov.standardPrimeAPMaxError_one (x : ℕ) :
          standardPrimeAPMaxError x 1 = |standardPrimeAPError x 1 0|
          source
          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.

          source
          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
          Instances For
            source
            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.

            source
            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.

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

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

            source
            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.

            source
            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.

            source
            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.

            source
            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
            Instances For
              source
              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.