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

• Nat.primesBelow n = Finset.filter (fun (p : ℕ) => Nat.Prime p) (Finset.range n)

@[simp]

theorem Nat.primesBelow_zero : Nat.primesBelow 0 = ∅

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

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

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

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

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

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 ∈ Nat.factors m, p ∈ s}

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

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

Membership in Nat.factoredNumbers n is decidable.

Equations

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

theorem Nat.mem_factoredNumbers_of_dvd {s : Finset ℕ} {m : ℕ} {k : ℕ} (h : m ∈ Nat.factoredNumbers s) (h' : k ∣ m) : k ∈ Nat.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 ∈ Nat.factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Nat.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 ∈ Nat.factoredNumbers s ↔ ∀ (p : ℕ), Nat.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 ∈ Nat.factoredNumbers s) : m ≠ 0

@[simp]

theorem Nat.factoredNumbers_empty : Nat.factoredNumbers ∅ = {1}

theorem Nat.prod_mem_factoredNumbers (s : Finset ℕ) (n : ℕ) : List.prod (List.filter (fun (x : ℕ) => decide (x ∈ s)) (Nat.factors n)) ∈ Nat.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 : ¬Nat.Prime N) : Nat.factoredNumbers (insert N s) = Nat.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 : Finset ℕ} {t : Finset ℕ} (hst : s ≤ t) : Nat.factoredNumbers s ⊆ Nat.factoredNumbers t

theorem Nat.factoredNumbers_compl {N : ℕ} {s : Finset ℕ} (h : Nat.primesBelow N ≤ s) : (Nat.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 : Nat.Prime p) (e : ℕ) (hn : n ∈ Nat.factoredNumbers s) : p ^ e * n ∈ Nat.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 : Nat.Prime p) (hs : p ∉ s) (hn : n ∈ Nat.factoredNumbers s) : Nat.Coprime p 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} [CommSemiring F] {f : ℕ → F} (hmul : ∀ {m n : ℕ}, Nat.Coprime m n → f (m * n) = f m * f n) {s : Finset ℕ} {p : ℕ} (hp : Nat.Prime p) (hs : p ∉ s) (e : ℕ) {m : ↑(Nat.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 : Nat.Prime p) (hs : p ∉ s) : ℕ × ↑(Nat.factoredNumbers s) ≃ ↑(Nat.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 : Nat.Prime p) (hs : p ∉ s) (hm : m ∈ Nat.factoredNumbers s) : ↑((Nat.equivProdNatFactoredNumbers hp hs) (e, { val := m, property := hm })) = p ^ e * m

@[simp]

theorem Nat.equivProdNatFactoredNumbers_apply' {s : Finset ℕ} {p : ℕ} (hp : Nat.Prime p) (hs : p ∉ s) (x : ℕ × ↑(Nat.factoredNumbers s)) : ↑((Nat.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

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

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

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

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

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

Membership in Nat.smoothNumbers n is decidable.

Equations

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

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

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

theorem Nat.mem_smoothNumbers_iff_forall_le {n : ℕ} {m : ℕ} : m ∈ Nat.smoothNumbers n ↔ m ≠ 0 ∧ ∀ p ≤ m, Nat.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 ∈ Nat.smoothNumbers n ↔ ∀ (p : ℕ), Nat.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.ne_zero_of_mem_smoothNumbers {n : ℕ} {m : ℕ} (h : m ∈ Nat.smoothNumbers n) : m ≠ 0

@[simp]

theorem Nat.smoothNumbers_zero : Nat.smoothNumbers 0 = {1}

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

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

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

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 : Nat.smoothNumbers 1 = {1}

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

theorem Nat.smoothNumbers_compl (N : ℕ) : (Nat.smoothNumbers N)ᶜ \ {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 ∈ Nat.smoothNumbers p) : p ^ e * n ∈ Nat.smoothNumbers (Nat.succ p)

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 : Nat.Prime p) (hn : n ∈ Nat.smoothNumbers p) : Nat.Coprime p 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} [CommSemiring F] {f : ℕ → F} (hmul : ∀ {m n : ℕ}, Nat.Coprime m n → f (m * n) = f m * f n) {p : ℕ} (hp : Nat.Prime p) (e : ℕ) {m : ↑(Nat.smoothNumbers p)} : 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 : Nat.Prime p) : ℕ × ↑(Nat.smoothNumbers p) ≃ ↑(Nat.smoothNumbers (Nat.succ p))

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 : Nat.Prime p) (hm : m ∈ Nat.smoothNumbers p) : ↑((Nat.equivProdNatSmoothNumbers hp) (e, { val := m, property := hm })) = p ^ e * m

@[simp]

theorem Nat.equivProdNatSmoothNumbers_apply' {p : ℕ} (hp : Nat.Prime p) (x : ℕ × ↑(Nat.smoothNumbers p)) : ↑((Nat.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

• Nat.smoothNumbersUpTo N k = Finset.filter (fun (x : ℕ) => x ∈ Nat.smoothNumbers k) (Finset.range (Nat.succ N))

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

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

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

Equations

• Nat.roughNumbersUpTo N k = Finset.filter (fun (n : ℕ) => n ≠ 0 ∧ n ∉ Nat.smoothNumbers k) (Finset.range (Nat.succ N))

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

theorem Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers {n : ℕ} {k : ℕ} (h : n ∈ Nat.smoothNumbers k) : ∃ s ∈ Finset.powerset (Nat.primesBelow k), ∃ (m : ℕ), n = m ^ 2 * Finset.prod s 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 : ℕ) : Nat.smoothNumbersUpTo N k ⊆ Finset.image (fun (x : Finset ℕ × ℕ) => match x with | (s, m) => m ^ 2 * Finset.prod s id) (Finset.powerset (Nat.primesBelow k) ×ˢ Finset.erase (Finset.range (Nat.succ (Nat.sqrt N))) 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 : ℕ) : (Nat.smoothNumbersUpTo N k).card ≤ 2 ^ (Nat.primesBelow k).card * Nat.sqrt N

The cardinality of the set of k-smooth numbers ≤ N is bounded by 2^π(k-1) * √N.

theorem Nat.roughNumbersUpTo_eq_biUnion (N : ℕ) (k : ℕ) : Nat.roughNumbersUpTo N k = Finset.biUnion (Nat.primesBelow (Nat.succ N) \ Nat.primesBelow k) fun (p : ℕ) => Finset.filter (fun (m : ℕ) => m ≠ 0 ∧ p ∣ m) (Finset.range (Nat.succ N))

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 : ℕ) : (Nat.roughNumbersUpTo N k).card ≤ Finset.sum (Nat.primesBelow (Nat.succ N) \ Nat.primesBelow k) fun (p : ℕ) => 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.