Commit 2025-09-01 17:39 2580ac69

View on Github →

chore(NumberTheory/SelbergSieve): turn BoundingSieve into a struct (#27820) Based on a discussion on zulip. I wound up removing the custom notation as well, since not everybody was fond of it and I had some trouble getting it to work properly with structure inheritance and the corresponding coersions.

Estimated changes

Modified Mathlib/NumberTheory/SelbergSieve.lean

added def BoundingSieve.IsUpperMoebius

added def BoundingSieve.errSum

added def BoundingSieve.mainSum

added def BoundingSieve.multSum

added theorem BoundingSieve.multSum_eq_main_err

added theorem BoundingSieve.nu_lt_one_of_dvd_prodPrimes

added theorem BoundingSieve.nu_ne_zero

added theorem BoundingSieve.nu_pos_of_dvd_prodPrimes

added theorem BoundingSieve.one_le_y

added theorem BoundingSieve.prodPrimes_ne_zero

added theorem BoundingSieve.prod_primeFactors_nu

added def BoundingSieve.rem

added def BoundingSieve.siftedSum

added theorem BoundingSieve.siftedSum_eq_sum_support_mul_ite

added theorem BoundingSieve.siftedSum_le_mainSum_errSum_of_upperMoebius

added theorem BoundingSieve.siftedSum_le_sum_of_upperMoebius

added theorem BoundingSieve.squarefree_of_dvd_prodPrimes

added theorem BoundingSieve.squarefree_of_mem_divisors_prodPrimes

added structure BoundingSieve

deleted def SelbergSieve.IsUpperMoebius

deleted theorem SelbergSieve.Notation.one_le_y

deleted def SelbergSieve.errSum

deleted def SelbergSieve.mainSum

deleted def SelbergSieve.multSum

deleted theorem SelbergSieve.multSum_eq_main_err

deleted theorem SelbergSieve.nu_lt_one_of_dvd_prodPrimes

deleted theorem SelbergSieve.nu_ne_zero

deleted theorem SelbergSieve.nu_pos_of_dvd_prodPrimes

deleted theorem SelbergSieve.prodPrimes_ne_zero

deleted theorem SelbergSieve.prod_primeFactors_nu

deleted def SelbergSieve.rem

deleted def SelbergSieve.siftedSum

deleted theorem SelbergSieve.siftedSum_eq_sum_support_mul_ite

deleted theorem SelbergSieve.siftedSum_le_mainSum_errSum_of_upperMoebius

deleted theorem SelbergSieve.siftedSum_le_sum_of_upperMoebius

deleted theorem SelbergSieve.squarefree_of_dvd_prodPrimes

deleted theorem SelbergSieve.squarefree_of_mem_divisors_prodPrimes

added structure SelbergSieve