Documentation

Mathlib.NumberTheory.SmoothNumbers

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.

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

Equations
theorem Nat.lt_of_mem_primesBelow {p n : } (h : p n.primesBelow) :
p < n
@[deprecated Nat.notMem_primesBelow (since := "2025-05-23")]
theorem Nat.not_mem_primesBelow (n : ) :
nn.primesBelow

Alias of Nat.notMem_primesBelow.

s-factored numbers #

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
theorem Nat.mem_factoredNumbers_of_dvd {s : Finset } {m k : } (h : m factoredNumbers s) (h' : k m) :

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 pm, Prime pp mp 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 pp mp s

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

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

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

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

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

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

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.

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) :

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 : ps) (hn : n factoredNumbers s) :

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 nf (m * n) = f m * f n) {s : Finset } {p : } (hp : Prime p) (hs : ps) (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 : ps) :

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 : ps) (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 : ps) (x : × (factoredNumbers s)) :
((equivProdNatFactoredNumbers hp hs) x) = p ^ x.1 * x.2

n-smooth numbers #

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
theorem Nat.mem_smoothNumbers {n m : } :
m n.smoothNumbers m 0 pm.primeFactorsList, p < n

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

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

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

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 pm, Prime pp mp < 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 pp mp < n

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

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

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

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

Zero is never a smooth number

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.

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

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.

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

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

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) :

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) :

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 nf (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.

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
@[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.

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

Equations

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

Equations
theorem Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers {n k : } (h : n k.smoothNumbers) :
sk.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.

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 : ) => {mFinset.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.