Theorems · Theorem · number theory
Nat.smoothNumbersUpTo_card_le
∀ (N k : ℕ), (N.smoothNumbersUpTo k).card ≤ 2 ^ k.primesBelow.card * N.sqrt
The cardinality of the set of k-smooth numbers ≤ N is bounded by 2^π(k-1) * √N.
- Defined in
- Mathlib.NumberTheory.SmoothNumbers
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LE.le.transproof · cited by 3,151
- Finset.cardstatement and proof · cited by 2,327
- SProd.sprodproof · cited by 1,750
- Finset.rangeproof · cited by 1,341
- Finset.eraseproof · cited by 455
- Finset.card_le_cardproof · cited by 118
- Finset.card_rangeproof · cited by 108
- Finset.powersetproof · cited by 93
- Nat.primesBelowstatement and proof · cited by 43
- Finset.card_productproof · cited by 39
- Finset.card_erase_of_memproof · cited by 38
- Finset.card_image_leproof · cited by 33
Cited by1
Results whose statement or proof uses this declaration.
- one_half_le_sum_primes_ge_one_divproof · cited by 1