Brun's theorem

TheoremBrun's theorem on twin primes#✓fully proved

The series \(\sum_{p} \left(\frac{1}{p} + \frac{1}{p + 2}\right)\), taken over all primes \(p\) such that \(p + 2\) is also prime, converges in \(\mathbb{R}\).

Each twin-prime pair \((p, p + 2)\) is indexed by its smaller member, so a prime lying in two pairs, such as \(5\) in \((3, 5)\) and \((5, 7)\), is counted once for each pair. The statement holds trivially if there are only finitely many twin-prime pairs.

theorem brun_twin_prime_reciprocal_series_summable :
    Summable (fun p : ℕ =>
      if p.Prime ∧ (p + 2).Prime then
        (1 : ℝ) / (p : ℝ) + (1 : ℝ) / ((p + 2 : ℕ) : ℝ)
      else 0)
Sources
Uses 7 · Used by 1
Proof usesSelberg level set · Selberg level sum · The Selberg level sum is at least one · Selberg sieve weights · Error bound for the Selberg level weights · Main term of the Selberg level weights · The Selberg level weight at one
Used bySummability of the twin-prime reciprocal terms

DefinitionTwin-prime reciprocal term#✓fully proved

For a natural number \(p\), the twin-prime reciprocal term \(t(p)\) is the real number \(\frac{1}{p} + \frac{1}{p + 2}\) when \(p\) and \(p + 2\) are both prime, and \(0\) otherwise.

noncomputable def brunTwinPrimeReciprocalTerm (p : ℕ) : ℝ :=
  if p.Prime ∧ (p + 2).Prime then
    (1 : ℝ) / (p : ℝ) + (1 : ℝ) / ((p + 2 : ℕ) : ℝ)
  else 0
Sources
  • teorth/optimizationproblems, “Brun's Constant,” constants/81a.md; the convention counts a prime once for every twin-prime pair containing it.
Used by 3
Used byBrun's constant · Brun's constant is the sum of the twin-prime reciprocal series · Summability of the twin-prime reciprocal terms

TheoremSummability of the twin-prime reciprocal terms#✓fully proved

For a natural number \(p\), let \(t(p)\) be \(\frac{1}{p} + \frac{1}{p + 2}\) when \(p\) and \(p + 2\) are both prime and \(0\) otherwise. Then the series \(\sum_{p \ge 0} t(p)\) converges unconditionally in \(\mathbb{R}\).

theorem summable_brunTwinPrimeReciprocalTerm :
    Summable brunTwinPrimeReciprocalTerm
Uses 2 · Used by 1
Statement usesTwin-prime reciprocal term
Proof usesBrun's theorem on twin primes
Used byBrun's constant is the sum of the twin-prime reciprocal series

DefinitionBrun's constant#✓fully proved

Brun's constant is the real number \(B = \sum_{p} \left(\frac{1}{p} + \frac{1}{p + 2}\right)\), the sum over all primes \(p\) such that \(p + 2\) is also prime. A prime lying in two twin-prime pairs, such as \(5\) in \((3, 5)\) and \((5, 7)\), is counted once for each pair.

noncomputable def brunConstant : ℝ :=
  ∑' p : ℕ, brunTwinPrimeReciprocalTerm p
Uses 1 · Used by 3
Statement usesTwin-prime reciprocal term
Used byLower bound for Brun's constant · Upper bound for Brun's constant · Brun's constant is the sum of the twin-prime reciprocal series

TheoremBrun's constant is the sum of the twin-prime reciprocal series#✓fully proved

For a natural number \(p\), let \(t(p)\) be \(\frac{1}{p} + \frac{1}{p + 2}\) when \(p\) and \(p + 2\) are both prime and \(0\) otherwise. Then the series \(\sum_{p \ge 0} t(p)\) over the natural numbers converges unconditionally in \(\mathbb{R}\), and its sum is Brun's constant.

theorem hasSum_brunConstant :
    HasSum brunTwinPrimeReciprocalTerm brunConstant
Uses 3
Statement usesBrun's constant · Twin-prime reciprocal term
Proof usesSummability of the twin-prime reciprocal terms

TheoremLower bound for Brun's constant#●ready to prove

Brun's constant \(B\), the sum of \(\frac{1}{p} + \frac{1}{p + 2}\) over all primes \(p\) such that \(p + 2\) is also prime, satisfies \(B > 1.840503\).

public theorem_wanted brunConstant_lower_bound :
    1.840503 < brunConstant
Sources
  • Dave Platt and Tim Trudgian, “Improved bounds on Brun's constant,” Experimental Mathematics 28 (2019), no. 2, 179–184; arXiv:1803.01925. The bound is also recorded in teorth/optimizationproblems, constants/81a.md.
Uses 1
Statement usesBrun's constant

TheoremUpper bound for Brun's constant#●ready to prove

Brun's constant \(B\), the sum of \(\frac{1}{p} + \frac{1}{p + 2}\) over all primes \(p\) such that \(p + 2\) is also prime, satisfies \(B < 2.288513\).

public theorem_wanted brunConstant_upper_bound :
    brunConstant < 2.288513
Sources
  • Dave Platt and Tim Trudgian, “Improved bounds on Brun's constant,” Experimental Mathematics 28 (2019), no. 2, 179–184; arXiv:1803.01925. The bound is also recorded in teorth/optimizationproblems, constants/81a.md.
Uses 1
Statement usesBrun's constant
5 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.