Smooth numbers

For s : Finset ℕ we define the set Nat.factoredNumbers s of "s-factored numbers" consisting of the positive natural numbers all of whose prime factors are in s, and we provide some API for this.

We then define the set Nat.smoothNumbers n consisting of the positive natural numbers all of whose prime factors are strictly less than n. This is the special case s = Finset.range n of the set of s-factored numbers.

We also define the finite set Nat.primesBelow n to be the set of prime numbers less than n.

The main definition Nat.equivProdNatSmoothNumbers establishes the bijection between ℕ × (smoothNumbers p) and smoothNumbers (p+1) given by sending (e, n) to p^e * n. Here p is a prime number. It is obtained from the more general bijection between ℕ × (factoredNumbers s) and factoredNumbers (s ∪ {p}); see Nat.equivProdNatFactoredNumbers.

Additionally, we define Nat.smoothNumbersUpTo N n as the Finset of n-smooth numbers up to and including N, and similarly Nat.roughNumbersUpTo for its complement in {1, ..., N}, and we provide some API, in particular bounds for their cardinalities; see Nat.smoothNumbersUpTo_card_le and Nat.roughNumbersUpTo_card_le.

def Nat.primesBelow (n : ℕ) : Finset ℕ

primesBelow n is the set of primes less than n as a Finset.

Equations

• n.primesBelow = {p ∈ Finset.range n | Nat.Prime p}

@[simp]

theorem Nat.primesBelow_zero : primesBelow 0 = ∅

theorem Nat.mem_primesBelow {k n : ℕ} : n ∈ k.primesBelow ↔ n < k ∧ Prime n

theorem Nat.prime_of_mem_primesBelow {p n : ℕ} (h : p ∈ n.primesBelow) : Prime p

theorem Nat.lt_of_mem_primesBelow {p n : ℕ} (h : p ∈ n.primesBelow) : p < n

theorem Nat.primesBelow_succ (n : ℕ) : (n + 1).primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow

theorem Nat.notMem_primesBelow (n : ℕ) : n ∉ n.primesBelow

@[deprecated Nat.notMem_primesBelow (since := "2025-05-23")]

theorem Nat.not_mem_primesBelow (n : ℕ) : n ∉ n.primesBelow

Alias of Nat.notMem_primesBelow.

s-factored numbers

def Nat.factoredNumbers (s : Finset ℕ) : Set ℕ

factoredNumbers s, for a finite set s of natural numbers, is the set of positive natural numbers all of whose prime factors are in s.

Equations

• Nat.factoredNumbers s = {m : ℕ | m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s}

theorem Nat.mem_factoredNumbers {s : Finset ℕ} {m : ℕ} : m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s

instance Nat.instDecidablePredMemSetFactoredNumbers (s : Finset ℕ) : DecidablePred fun (x : ℕ) => x ∈ factoredNumbers s

Membership in Nat.factoredNumbers n is decidable.

Equations

• Nat.instDecidablePredMemSetFactoredNumbers s = inferInstanceAs (DecidablePred fun (x : ℕ) => x ∈ {m : ℕ | m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s})

theorem Nat.mem_factoredNumbers_of_dvd {s : Finset ℕ} {m k : ℕ} (h : m ∈ factoredNumbers s) (h' : k ∣ m) : k ∈ factoredNumbers s

A number that divides an s-factored number is itself s-factored.

theorem Nat.mem_factoredNumbers_iff_forall_le {s : Finset ℕ} {m : ℕ} : m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s

m is s-factored if and only if m is nonzero and all prime divisors ≤ m of m are in s.

theorem Nat.mem_factoredNumbers' {s : Finset ℕ} {m : ℕ} : m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

m is s-factored if and only if all prime divisors of m are in s.

theorem Nat.ne_zero_of_mem_factoredNumbers {s : Finset ℕ} {m : ℕ} (h : m ∈ factoredNumbers s) : m ≠ 0

theorem Nat.primeFactors_subset_of_mem_factoredNumbers {s : Finset ℕ} {m : ℕ} (hm : m ∈ factoredNumbers s) : m.primeFactors ⊆ s

The Finset of prime factors of an s-factored number is contained in s.

theorem Nat.mem_factoredNumbers_of_primeFactors_subset {s : Finset ℕ} {m : ℕ} (hm : m ≠ 0) (hp : m.primeFactors ⊆ s) : m ∈ factoredNumbers s

If m ≠ 0 and the Finset of prime factors of m is contained in s, then m is s-factored.

theorem Nat.mem_factoredNumbers_iff_primeFactors_subset {s : Finset ℕ} {m : ℕ} : m ∈ factoredNumbers s ↔ m ≠ 0 ∧ m.primeFactors ⊆ s

m is s-factored if and only if m ≠ 0 and its Finset of prime factors is contained in s.

@[simp]

theorem Nat.factoredNumbers_empty : factoredNumbers ∅ = {1}

theorem Nat.mul_mem_factoredNumbers {s : Finset ℕ} {m n : ℕ} (hm : m ∈ factoredNumbers s) (hn : n ∈ factoredNumbers s) : m * n ∈ factoredNumbers s

The product of two s-factored numbers is again s-factored.

theorem Nat.prod_mem_factoredNumbers (s : Finset ℕ) (n : ℕ) : (List.filter (fun (x : ℕ) => decide (x ∈ s)) n.primeFactorsList).prod ∈ factoredNumbers s

The product of the prime factors of n that are in s is an s-factored number.

theorem Nat.factoredNumbers_insert (s : Finset ℕ) {N : ℕ} (hN : ¬Prime N) : factoredNumbers (insert N s) = factoredNumbers s

The sets of s-factored and of s ∪ {N}-factored numbers are the same when N is not prime. See Nat.equivProdNatFactoredNumbers for when N is prime.

theorem Nat.factoredNumbers_mono {s t : Finset ℕ} (hst : s ≤ t) : factoredNumbers s ⊆ factoredNumbers t

theorem Nat.factoredNumbers_compl {N : ℕ} {s : Finset ℕ} (h : N.primesBelow ≤ s) : (factoredNumbers s)ᶜ \ {0} ⊆ {n : ℕ | N ≤ n}

The non-zero non-s-factored numbers are ≥ N when s contains all primes less than N.

theorem Nat.pow_mul_mem_factoredNumbers {s : Finset ℕ} {p n : ℕ} (hp : Prime p) (e : ℕ) (hn : n ∈ factoredNumbers s) : p ^ e * n ∈ factoredNumbers (insert p s)

If p is a prime and n is s-factored, then every product p^e * n is s ∪ {p}-factored.

theorem Nat.Prime.factoredNumbers_coprime {s : Finset ℕ} {p n : ℕ} (hp : Prime p) (hs : p ∉ s) (hn : n ∈ factoredNumbers s) : p.Coprime n

If p ∉ s is a prime and n is s-factored, then p and n are coprime.

theorem Nat.factoredNumbers.map_prime_pow_mul {F : Type u_1} [Mul F] {f : ℕ → F} (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) {s : Finset ℕ} {p : ℕ} (hp : Prime p) (hs : p ∉ s) (e : ℕ) {m : ↑(factoredNumbers s)} : f (p ^ e * ↑m) = f (p ^ e) * f ↑m

If f : ℕ → F is multiplicative on coprime arguments, p ∉ s is a prime and m is s-factored, then f (p^e * m) = f (p^e) * f m.

def Nat.equivProdNatFactoredNumbers {s : Finset ℕ} {p : ℕ} (hp : Prime p) (hs : p ∉ s) : ℕ × ↑(factoredNumbers s) ≃ ↑(factoredNumbers (insert p s))

We establish the bijection from ℕ × factoredNumbers s to factoredNumbers (s ∪ {p}) given by (e, n) ↦ p^e * n when p ∉ s is a prime. See Nat.factoredNumbers_insert for when p is not prime.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Nat.equivProdNatFactoredNumbers_apply {s : Finset ℕ} {p e m : ℕ} (hp : Prime p) (hs : p ∉ s) (hm : m ∈ factoredNumbers s) : ↑((equivProdNatFactoredNumbers hp hs) (e, ⟨m, hm⟩)) = p ^ e * m

@[simp]

theorem Nat.equivProdNatFactoredNumbers_apply' {s : Finset ℕ} {p : ℕ} (hp : Prime p) (hs : p ∉ s) (x : ℕ × ↑(factoredNumbers s)) : ↑((equivProdNatFactoredNumbers hp hs) x) = p ^ x.1 * ↑x.2

n-smooth numbers

def Nat.smoothNumbers (n : ℕ) : Set ℕ

smoothNumbers n is the set of n-smooth positive natural numbers, i.e., the positive natural numbers all of whose prime factors are less than n.

Equations

• n.smoothNumbers = {m : ℕ | m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p < n}

theorem Nat.mem_smoothNumbers {n m : ℕ} : m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p < n

theorem Nat.smoothNumbers_eq_factoredNumbers (n : ℕ) : n.smoothNumbers = factoredNumbers (Finset.range n)

The n-smooth numbers agree with the Finset.range n-factored numbers.

theorem Nat.smoothNumbers_eq_factoredNumbers_primesBelow (n : ℕ) : n.smoothNumbers = factoredNumbers n.primesBelow

The n-smooth numbers agree with the primesBelow n-factored numbers.

@[deprecated Nat.smoothNumbers_eq_factoredNumbers_primesBelow (since := "2025-07-08")]

theorem Nat.smmoothNumbers_eq_factoredNumbers_primesBelow (n : ℕ) : n.smoothNumbers = factoredNumbers n.primesBelow

Alias of Nat.smoothNumbers_eq_factoredNumbers_primesBelow.

---

The n-smooth numbers agree with the primesBelow n-factored numbers.

instance Nat.instDecidablePredMemSetSmoothNumbers (n : ℕ) : DecidablePred fun (x : ℕ) => x ∈ n.smoothNumbers

Membership in Nat.smoothNumbers n is decidable.

Equations

• n.instDecidablePredMemSetSmoothNumbers = inferInstanceAs (DecidablePred fun (x : ℕ) => x ∈ {m : ℕ | m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p < n})

theorem Nat.mem_smoothNumbers_of_dvd {n m k : ℕ} (h : m ∈ n.smoothNumbers) (h' : k ∣ m) : k ∈ n.smoothNumbers

A number that divides an n-smooth number is itself n-smooth.

theorem Nat.mem_smoothNumbers_iff_forall_le {n m : ℕ} : m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p < n

m is n-smooth if and only if m is nonzero and all prime divisors ≤ m of m are less than n.

theorem Nat.mem_smoothNumbers' {n m : ℕ} : m ∈ n.smoothNumbers ↔ ∀ (p : ℕ), Prime p → p ∣ m → p < n

m is n-smooth if and only if all prime divisors of m are less than n.

theorem Nat.primeFactors_subset_of_mem_smoothNumbers {m n : ℕ} (hms : m ∈ n.smoothNumbers) : m.primeFactors ⊆ n.primesBelow

The Finset of prime factors of an n-smooth number is contained in the Finset of primes below n.

theorem Nat.mem_smoothNumbers_of_primeFactors_subset {m n : ℕ} (hm : m ≠ 0) (hp : m.primeFactors ⊆ Finset.range n) : m ∈ n.smoothNumbers

m is an n-smooth number if the Finset of its prime factors consists of numbers < n.

theorem Nat.mem_smoothNumbers_iff_primeFactors_subset {m n : ℕ} : m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ m.primeFactors ⊆ n.primesBelow

m is an n-smooth number if and only if m ≠ 0 and the Finset of its prime factors is contained in the Finset of primes below n

theorem Nat.ne_zero_of_mem_smoothNumbers {n m : ℕ} (h : m ∈ n.smoothNumbers) : m ≠ 0

Zero is never a smooth number

@[simp]

theorem Nat.smoothNumbers_zero : smoothNumbers 0 = {1}

theorem Nat.mul_mem_smoothNumbers {m₁ m₂ n : ℕ} (hm1 : m₁ ∈ n.smoothNumbers) (hm2 : m₂ ∈ n.smoothNumbers) : m₁ * m₂ ∈ n.smoothNumbers

The product of two n-smooth numbers is an n-smooth number.

theorem Nat.prod_mem_smoothNumbers (n N : ℕ) : (List.filter (fun (x : ℕ) => decide (x < N)) n.primeFactorsList).prod ∈ N.smoothNumbers

The product of the prime factors of n that are less than N is an N-smooth number.

theorem Nat.smoothNumbers_succ {N : ℕ} (hN : ¬Prime N) : (N + 1).smoothNumbers = N.smoothNumbers

The sets of N-smooth and of (N+1)-smooth numbers are the same when N is not prime. See Nat.equivProdNatSmoothNumbers for when N is prime.

@[simp]

theorem Nat.smoothNumbers_one : smoothNumbers 1 = {1}

theorem Nat.smoothNumbers_mono {N M : ℕ} (hNM : N ≤ M) : N.smoothNumbers ⊆ M.smoothNumbers

theorem Nat.mem_smoothNumbers_of_lt {m n : ℕ} (hm : 0 < m) (hmn : m < n) : m ∈ n.smoothNumbers

All m, 0 < m < n are n-smooth numbers

theorem Nat.smoothNumbers_compl (N : ℕ) : N.smoothNumbersᶜ \ {0} ⊆ {n : ℕ | N ≤ n}

The non-zero non-N-smooth numbers are ≥ N.

theorem Nat.pow_mul_mem_smoothNumbers {p n : ℕ} (hp : p ≠ 0) (e : ℕ) (hn : n ∈ p.smoothNumbers) : p ^ e * n ∈ p.succ.smoothNumbers

If p is positive and n is p-smooth, then every product p^e * n is (p+1)-smooth.

theorem Nat.Prime.smoothNumbers_coprime {p n : ℕ} (hp : Prime p) (hn : n ∈ p.smoothNumbers) : p.Coprime n

If p is a prime and n is p-smooth, then p and n are coprime.

theorem Nat.map_prime_pow_mul {F : Type u_1} [Mul F] {f : ℕ → F} (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) {p : ℕ} (hp : Prime p) (e : ℕ) {m : ↑p.smoothNumbers} : f (p ^ e * ↑m) = f (p ^ e) * f ↑m

If f : ℕ → F is multiplicative on coprime arguments, p is a prime and m is p-smooth, then f (p^e * m) = f (p^e) * f m.

def Nat.equivProdNatSmoothNumbers {p : ℕ} (hp : Prime p) : ℕ × ↑p.smoothNumbers ≃ ↑(p + 1).smoothNumbers

We establish the bijection from ℕ × smoothNumbers p to smoothNumbers (p+1) given by (e, n) ↦ p^e * n when p is a prime. See Nat.smoothNumbers_succ for when p is not prime.

Equations

• Nat.equivProdNatSmoothNumbers hp = ((Equiv.prodCongrRight fun (x : ℕ) => Equiv.setCongr ⋯).trans (Nat.equivProdNatFactoredNumbers hp ⋯)).trans (Equiv.setCongr ⋯)

@[simp]

theorem Nat.equivProdNatSmoothNumbers_apply {p e m : ℕ} (hp : Prime p) (hm : m ∈ p.smoothNumbers) : ↑((equivProdNatSmoothNumbers hp) (e, ⟨m, hm⟩)) = p ^ e * m

@[simp]

theorem Nat.equivProdNatSmoothNumbers_apply' {p : ℕ} (hp : Prime p) (x : ℕ × ↑p.smoothNumbers) : ↑((equivProdNatSmoothNumbers hp) x) = p ^ x.1 * ↑x.2

Smooth and rough numbers up to a bound

We consider the sets of smooth and non-smooth ("rough") positive natural numbers ≤ N and prove bounds for their sizes.

def Nat.smoothNumbersUpTo (N k : ℕ) : Finset ℕ

The k-smooth numbers up to and including N as a Finset

Equations

• N.smoothNumbersUpTo k = {n ∈ Finset.range (N + 1) | n ∈ k.smoothNumbers}

theorem Nat.mem_smoothNumbersUpTo {N k n : ℕ} : n ∈ N.smoothNumbersUpTo k ↔ n ≤ N ∧ n ∈ k.smoothNumbers

def Nat.roughNumbersUpTo (N k : ℕ) : Finset ℕ

The positive non-k-smooth (so "k-rough") numbers up to and including N as a Finset

Equations

• N.roughNumbersUpTo k = {n ∈ Finset.range (N + 1) | n ≠ 0 ∧ n ∉ k.smoothNumbers}

theorem Nat.smoothNumbersUpTo_card_add_roughNumbersUpTo_card (N k : ℕ) : (N.smoothNumbersUpTo k).card + (N.roughNumbersUpTo k).card = N

theorem Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers {n k : ℕ} (h : n ∈ k.smoothNumbers) : ∃ s ∈ k.primesBelow.powerset, ∃ (m : ℕ), n = m ^ 2 * s.prod id

A k-smooth number can be written as a square times a product of distinct primes < k.

theorem Nat.smoothNumbersUpTo_subset_image (N k : ℕ) : N.smoothNumbersUpTo k ⊆ Finset.image (fun (x : Finset ℕ × ℕ) => match x with | (s, m) => m ^ 2 * s.prod id) (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)

The set of k-smooth numbers ≤ N is contained in the set of numbers of the form m^2 * P, where m ≤ √N and P is a product of distinct primes < k.

theorem 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.

theorem Nat.roughNumbersUpTo_eq_biUnion (N k : ℕ) : N.roughNumbersUpTo k = ((N + 1).primesBelow \ k.primesBelow).biUnion fun (p : ℕ) => {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}

The set of k-rough numbers ≤ N can be written as the union of the sets of multiples ≤ N of primes k ≤ p ≤ N.

theorem Nat.roughNumbersUpTo_card_le (N k : ℕ) : (N.roughNumbersUpTo k).card ≤ ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p

The cardinality of the set of k-rough numbers ≤ N is bounded by the sum of ⌊N/p⌋ over the primes k ≤ p ≤ N.