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

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

Equations
Instances For
@[simp]
theorem Nat.mem_primesBelow {k : } {n : } :
n k.primesBelow n < k
theorem Nat.prime_of_mem_primesBelow {p : } {n : } (h : p n.primesBelow) :
theorem Nat.lt_of_mem_primesBelow {p : } {n : } (h : p n.primesBelow) :
p < n
theorem Nat.primesBelow_succ (n : ) :
n.succ.primesBelow = if then insert n n.primesBelow else n.primesBelow
theorem Nat.not_mem_primesBelow (n : ) :
nn.primesBelow

### s-factored numbers #

def Nat.factoredNumbers (s : ) :

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
Instances For
theorem Nat.mem_factoredNumbers {s : } {m : } :
m 0 pm.factors, p s

Membership in Nat.factoredNumbers n is decidable.

Equations
theorem Nat.mem_factoredNumbers_of_dvd {s : } {m : } {k : } (h : ) (h' : k m) :

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

theorem Nat.mem_factoredNumbers_iff_forall_le {s : } {m : } :
m 0 pm, p 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 : } {m : } :
∀ (p : ), p mp 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 : } {m : } (h : ) :
m 0
theorem Nat.primeFactors_subset_of_mem_factoredNumbers {s : } {m : } (hm : ) :
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 : } {m : } (hm : m 0) (hp : m.primeFactors 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 : } {m : } :
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.

theorem Nat.mul_mem_factoredNumbers {s : } {m : } {n : } (hm : ) (hn : ) :
m * n

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

theorem Nat.prod_mem_factoredNumbers (s : ) (n : ) :
(List.filter (fun (x : ) => decide (x s)) n.factors).prod

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

theorem Nat.factoredNumbers_insert (s : ) {N : } (hN : ) :

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 : } (hst : s t) :
theorem Nat.factoredNumbers_compl {N : } {s : } (h : N.primesBelow 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 : } {p : } {n : } (hp : ) (e : ) (hn : ) :
p ^ e * n

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 : } {p : } {n : } (hp : ) (hs : ps) (hn : ) :
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} [] {f : F} (hmul : ∀ {m n : }, m.Coprime nf (m * n) = f m * f n) {s : } {p : } (hp : ) (hs : ps) (e : ) {m : } :
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 : } {p : } (hp : ) (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.
Instances For
@[simp]
theorem Nat.equivProdNatFactoredNumbers_apply {s : } {p : } {e : } {m : } (hp : ) (hs : ps) (hm : ) :
(() (e, m, hm)) = p ^ e * m
@[simp]
theorem Nat.equivProdNatFactoredNumbers_apply' {s : } {p : } (hp : ) (hs : ps) (x : ) :
(() 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
• n.smoothNumbers = {m : | m 0 pm.factors, p < n}
Instances For
theorem Nat.mem_smoothNumbers {n : } {m : } :
m n.smoothNumbers m 0 pm.factors, p < n
theorem Nat.smoothNumbers_eq_factoredNumbers (n : ) :
n.smoothNumbers =

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

theorem Nat.smmoothNumbers_eq_factoredNumbers_primesBelow (n : ) :
n.smoothNumbers = Nat.factoredNumbers n.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
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 pm, p 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 : ), p mp < 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 ) :
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.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.factors).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 : ) :
N.succ.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 :
= {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 : ) (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} [] {f : F} (hmul : ∀ {m n : }, m.Coprime nf (m * n) = f m * f n) {p : } (hp : ) (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 : ) :
× p.smoothNumbers p.succ.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
Instances For
@[simp]
theorem Nat.equivProdNatSmoothNumbers_apply {p : } {e : } {m : } (hp : ) (hm : m p.smoothNumbers) :
( (e, m, hm)) = p ^ e * m
@[simp]
theorem Nat.equivProdNatSmoothNumbers_apply' {p : } (hp : ) (x : × p.smoothNumbers) :
() = 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 : ) :

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

Equations
Instances For
theorem Nat.mem_smoothNumbersUpTo {N : } {k : } {n : } :
n N.smoothNumbersUpTo k n N n k.smoothNumbers
def Nat.roughNumbersUpTo (N : ) (k : ) :

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

Equations
Instances For
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) :
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 : ) => match x with | (s, m) => m ^ 2 * s.prod id) (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).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.succ.primesBelow \ k.primesBelow).biUnion fun (p : ) => Finset.filter (fun (m : ) => m 0 p m) (Finset.range N.succ)

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 pN.succ.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.