brun_constant_converges.toml

id = "brun_constant_converges"
title = "Brun's theorem (convergence of the twin-prime reciprocal sum)"
test = false
module = "LeanEval.NumberTheory.BrunConstant"
holes = ["brun_constant_converges"]
submitter = "Kim Morrison"
notes = "Brun's theorem: the sum of the reciprocals of the twin primes converges, to a value now known as Brun's constant. The statement is phrased via a per-pair reciprocal term `twinPrimeReciprocalTerm p`, which contributes `1/p + 1/(p+2)` when `p` starts a twin pair and `0` otherwise, and asserts that this function is `Summable`. mathlib has `Nat.Prime`, `Summable`, and prime-counting estimates, but no Brun sieve."
source = "V. Brun, La série 1/5+1/7+1/11+1/13+... où les dénominateurs sont nombres premiers jumeaux est convergente ou finie, Bull. Sci. Math. 43 (1919), 100-104, 124-128. Listed as §224 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Knill, §224."
informal_solution = "Brun's sieve bounds the twin-prime counting function π₂(x) by O(x (log log x)² / (log x)²). Summing the reciprocals by dyadic blocks and applying this bound, the tail sums are dominated by a convergent series (essentially ∑ (log log n)² / (n (log n)²)), so the reciprocal sum over twin pairs converges."