Reservoir

1. selberg-sieve

The aim of this project is to formally verify the fundamental theorem of the Selberg sieve and prove some of its direct consequences. It was ported from this repo.

2. Build Instructions

TODO

3. Goals

I try to state the most important results and goals in MainResults.lean as I work on them.

We prove the following version of the Fundamental Theorem of the Selberg sieve as adapted from Heath-Brown.

Fundamental Theorem

Let be a finitely supported sequence of nonnegative real numbers, a squarefree number repersenting a finite set of primes, and a real number.

Suppose we can write where is multiplicative and for every prime .

Then where with And to get a better handle on we also show that if is completely multiplicative and all primes less than divide then

Prime counting function

To test this result, we prove that And in fact, with little addition effort we are able to prove the Brun-Titchmarsh type bound

We hope to later use this result to prove

Brun's Theorem

Let denote the number of twin primes at most . Then and as a corollary