Documentation

BV.MainResults

Bombieri-Vinogradov Theorem #

This module contains the formalization of the Bombieri-Vinogradov theorem, a fundamental result in analytic number theory.

Wrapping up

source
def C_BV_L (A : ℝ) :
ℝ
Equations
Instances For
    source
    theorem BV_Delta_Lambda [ProofData] (A : ℕ) (Q : ℝ) (h1Q : 1 ≤ Q) (hQ : Q ≤ √ProofData.x / Real.log ProofData.x ^ (A + 3)) :
    (∑ q ∈ Nat.Icc 0 Q, maxya q fun (y : ℝ) (a : ZMod q) => |Δ_[⇑ArithmeticFunction.vonMangoldt](y; q, a)|) ≤ C_BV_L ↑A * ProofData.x / Real.log ProofData.x ^ A
    source
    noncomputable def C_BV (A : ℕ) :
    ℝ

    Implied constant for Bombieri-Vinogradov theorem

    Equations
    Instances For
      source
      theorem bombieri_vinogradov (A : ℕ) {x : ℝ} (hx : 2 ≤ x) {Q : ℝ} (hle_Q : 1 ≤ Q) (hQ : Q ≤ √x / Real.log x ^ (A + 3)) :
      ∑ q ∈ Nat.Icc 1 Q, ⨆ y ∈ Set.Icc 1 x, ⨆ (a : (ZMod q)ˣ), |chebyPsi y ↑a - y / ↑q.totient| ≤ C_BV A * x / Real.log x ^ A