Smooth numbers

We define the set Nat.smoothNumbers n consisting of the positive natural numbers all of whose prime factors are strictly less than n.

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.

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

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

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

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

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