Commit 2025-03-19 14:32 b2684567

View on Github →

feat(NumberTheory): define the Selberg Sieve (#21880) This will be the first in a series of PRs proving the fundamental lemma of the Selberg sieve. This PR sets up the running assumptions for the Selberg sieve and writes the upper bound in terms of a main term and an error term.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/SelbergSieve.lean

added def SelbergSieve.IsUpperMoebius

added theorem SelbergSieve.Notation.one_le_y

added def SelbergSieve.errSum

added def SelbergSieve.mainSum

added def SelbergSieve.multSum

added theorem SelbergSieve.multSum_eq_main_err

added theorem SelbergSieve.nu_lt_one_of_dvd_prodPrimes

added theorem SelbergSieve.nu_ne_zero

added theorem SelbergSieve.nu_pos_of_dvd_prodPrimes

added theorem SelbergSieve.prodPrimes_ne_zero

added theorem SelbergSieve.prod_primeFactors_nu

added def SelbergSieve.rem

added def SelbergSieve.siftedSum

added theorem SelbergSieve.siftedSum_le_mainSum_errSum_of_upperMoebius

added theorem SelbergSieve.siftedSum_le_sum_of_upperMoebius

added theorem SelbergSieve.siftedsum_eq_sum_support_mul_ite

added theorem SelbergSieve.squarefree_of_dvd_prodPrimes

added theorem SelbergSieve.squarefree_of_mem_divisors_prodPrimes