Commit 2023-12-28 01:33 6cab3d64

View on Github →

feat(NumberTheory.SmoothNumbers): add {smooth|rough}NumbersUpTo and some API (#9240) This adds definitions of the k-smooth numbers up to and including N as a Finset and of its complement in {1, ..., N} plus some API, in particular cardinality bounds. There are also a few additional API lemmas for Nat.primesBelow and Nat.smoothNumbers (including a decidability instance for membership in the latter). This is a PR in preparation of the divergence of the sum of the reciprocals of the primes. See here on Zulip.

Estimated changes

Modified Mathlib/Data/Nat/Factorization/Basic.lean

added theorem Nat.card_multiples'

Modified Mathlib/NumberTheory/SmoothNumbers.lean

added theorem Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers

added theorem Nat.mem_primesBelow

added theorem Nat.mem_smoothNumbersUpTo

added theorem Nat.mem_smoothNumbers_iff_forall_le

added theorem Nat.mem_smoothNumbers_of_dvd

added theorem Nat.ne_zero_of_mem_smoothNumbers

added def Nat.roughNumbersUpTo

added theorem Nat.roughNumbersUpTo_card_le

added theorem Nat.roughNumbersUpTo_eq_biUnion

added def Nat.smoothNumbersUpTo

added theorem Nat.smoothNumbersUpTo_card_add_roughNumbersUpTo_card

added theorem Nat.smoothNumbersUpTo_card_le

added theorem Nat.smoothNumbersUpTo_subset_image