Theorems · Inductive type · number theory
BoundingSieve
Type
We set up a sieve problem as follows. Take a finite set of natural numbers A, whose elements
are weighted by a sequence a n. Also take a finite set of primes P, represented by a squarefree
natural number. These are the primes that we will sift from our set A. Suppose we can approximate
∑ n ∈ A with d ∣ n, a n = ν d * X + R d, where X is an approximation to the total size of A
and ν is a multiplicative arithmetic function such that 0 < ν p < 1 for all primes p ∣ P.
Then a sieve-type theorem will give us an upper (or lower) bound on the size of the sifted sum
∑ n ∈ support with n.Coprime P, a n, obtained by removing any elements of A that are a
multiple of a prime in P.
- Defined in
- Mathlib.NumberTheory.SelbergSieve
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by53
Results whose statement or proof uses this declaration.
- BoundingSieve.prodPrimesstatement and proof · cited by 18
- BoundingSieve.nustatement and proof · cited by 17
- BoundingSieve.selbergTermsstatement and proof · cited by 7
- BoundingSieve.prodPrimes_squarefreestatement and proof · cited by 6
- BoundingSieve.nu_multstatement and proof · cited by 4
- BoundingSieve.nu_pos_of_dvd_prodPrimesstatement and proof · cited by 4
- BoundingSieve.prodPrimes_ne_zerostatement and proof · cited by 4
- BoundingSieve.mainSumstatement and proof · cited by 3
- BoundingSieve.multSumstatement and proof · cited by 3
- BoundingSieve.siftedSumstatement and proof · cited by 3
- BoundingSieve.weightsstatement and proof · cited by 3
- BoundingSieve.nu_inv_eq_sum_divisors_inv_selbergTermsstatement and proof · cited by 2