Brun–Titchmarsh theorem

TheoremUniform Brun–Titchmarsh bound#✓fully proved

Write \(\pi(X; k, \ell)\) for the number of primes \(p \le X\) with \(p \equiv \ell \pmod{k}\), and \(\varphi\) for Euler's totient function. For every real \(\beta\) with \(0 < \beta < 1\) there is a real constant \(\xi_1 > 0\) such that for all natural numbers \(X\), \(k\) and \(\ell\) with \(X \ge 2\), \(k \ge 1\) and \(k \le X^{\beta}\),

\[ \pi(X; k, \ell) < \frac{\xi_1 X}{\varphi(k) \log(X/k)}. \]

No coprimality of \(k\) and \(\ell\) is assumed.

The proof applies Selberg's \(\Lambda^2\) upper-bound sieve to the arithmetic progression, with optimized weights and a harmonic lower bound for the diagonal sum.

public theorem brun_titchmarsh_uniform (β : ℝ) (hβ0 : 0 < β)
    (hβ1 : β < 1) :
    ∃ ξ₁ : ℝ, 0 < ξ₁ ∧ ∀ X k ell : ℕ, 2 ≤ X → 1 ≤ k →
      (k : ℝ) ≤ Real.rpow (X : ℝ) β →
      (Nat.primeCountingMod X k ell : ℝ) <
        ξ₁ * (X : ℝ) / ((Nat.totient k : ℝ) * Real.log ((X : ℝ) / (k : ℝ)))
Sources
  • Jean-Marie De Koninck and Imre Kátai, "Some Remarks on a Paper of L. Toth," Journal of Integer Sequences 13 (2010), https://cs.uwaterloo.ca/journals/JIS/VOL13/DeKoninck/dekoninck7.tex, Lemma, lines 424–429. The source cites E. C. Titchmarsh, "A divisor problem," Rend. Palermo 54 (1930), 414–429 and 57 (1933), 478–479. The bound 2 ≤ X makes the source's implicit analytic lower range explicit, and the source prints no coprimality hypothesis.
Uses 8
Statement usesPrime counting in a residue class
Proof usesSelberg level set · Selberg level sum · Selberg sieve weights · Error bound for the Selberg level weights · Main term of the Selberg level weights · The Selberg level weight at one · Residue-class prime count as a filtered range

TheoremLower bound for the squarefree totient sum#✓fully proved

For every natural number \(z \ge 6\), \(\log(z + 1) + 107/100 < \sum_{r=1}^{z} \mu(r)^2 / \varphi(r)\), where \(\mu\) is the Möbius function and \(\varphi\) is Euler's totient function.

public theorem moebiusSq_div_totient_sum_gt_log (z : ℕ) (hz : 6 ≤ z) :
    Real.log (z + 1) + 107 / 100 <
      ∑ r ∈ Finset.Icc 1 z,
        (((ArithmeticFunction.moebius r : ℤ) : ℝ) ^ 2 / Nat.totient r)
Sources
  • Montgomery–Vaughan, The large sieve (1973), Lemmas 4–7 and equation (4.3), lines 462–657. The bound here uses log (z + 1), which is slightly stronger than the paper's log z.
Used by 1
Used byWeighted lower bound for the squarefree totient sum

TheoremWeighted lower bound for the squarefree totient sum#✓fully proved

For every natural number \(z \ge 100\), \(\log z + 36/100 < \sum_{q=1}^{z} (1 + q/z)^{-1} \, \mu(q)^2 / \varphi(q)\), where \(\mu\) is the Möbius function and \(\varphi\) is Euler's totient function.

public theorem squarefreeTotientWeightedLower (z : ℕ) (hz : 100 ≤ z) :
    Real.log z + 36 / 100 <
      ∑ q ∈ Finset.Icc 1 z, (1 + (q : ℝ) / z)⁻¹ *
        (((ArithmeticFunction.moebius q : ℤ) : ℝ) ^ 2 / Nat.totient q)
Sources
  • Montgomery–Vaughan, The large sieve (1973), Lemma 8, lines 658–714. The proof uses Abel summation, moebiusSq_div_totient_sum_gt_log, and the paper's explicit correction from the terms q ≤ 5.
Uses 1 · Used by 1
Proof usesLower bound for the squarefree totient sum
Used byBrun–Titchmarsh inequality

TheoremBrun–Titchmarsh inequality#✓fully proved

Let \(X\), \(q\) and \(a\) be natural numbers such that \(a\) and \(q\) are coprime and \(1 \le q < X\). Write \(\pi(X; q, a)\) for the number of primes \(p \le X\) with \(p \equiv a \pmod{q}\), and \(\varphi\) for Euler's totient function. Then

\[ \pi(X; q, a) \le \frac{2X}{\varphi(q) \log(X/q)}. \]

The proof uses an elementary Eratosthenes sieve when \(X \le 20000q\). For larger \(X\) it combines the weighted arithmetic large sieve with explicit lower bounds for the squarefree-totient sum and the choice \(z = \lfloor \sqrt{2N/3} \rfloor\), where \(N = \lfloor X/q \rfloor + 1\).

public theorem brun_titchmarsh (X q a : ℕ) (haq : Nat.Coprime a q)
    (hq : 1 ≤ q) (hqX : q < X) :
    (Nat.primeCountingMod X q a : ℝ) ≤
      2 * (X : ℝ) / ((Nat.totient q : ℝ) * Real.log ((X : ℝ) / (q : ℝ)))
Sources
  • H. Iwaniec and E. Kowalski, Analytic Number Theory, AMS Colloquium Publications 53, 2004, Theorem 6.6; quoted as equation (1) in Y. Wang and X. Zhang, arXiv:2608.19262v1.
Uses 4
Statement usesPrime counting in a residue class
Proof usesArithmetic large sieve for primes in a progression · Weighted lower bound for the squarefree totient sum · Residue-class prime count as a filtered range
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.