The rough part of a number

A candidate for Mathlib.NumberTheory.SmoothNumbers: the part w of a number n at the primes from q on, n = k w with a q-smooth k (Nat.smoothNumbers) and a q-rough w, all of whose prime factors are at least q. It is the product of the prime factors of n ≠ 0 from q on, and dividing the part at the primes from the prime p on by the power of p leaves the part from p + 1 on, which is the part from the next prime on. Mathlib's Nat.roughNumbersUpTo says "rough" for "not smooth", a different notion.

Main definitions

• Nat.IsRoughPart: the part of a number at the primes from a bound on.

Main statements

• Nat.IsRoughPart.eq_prod_filter: the part of n ≠ 0 at the primes from q on is the product of its prime factors from q on.
• Nat.IsRoughPart.succ, Nat.IsRoughPart.of_le_of_forall: the part at the primes from the next prime on.

def Nat.IsRoughPart (q n w : ℕ) : Prop

w is the part of n at the primes from q on, its q-rough part: n = k w with a q-smooth k (every prime factor of k below q) and every prime factor of w at least q; for n ≠ 0 it is the product of the prime factors of n from q on, with multiplicity (Nat.IsRoughPart.eq_prod_filter).

Equations

• q.IsRoughPart n w = ∃ k ∈ q.smoothNumbers, n = k * w ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ w → q ≤ p

theorem Nat.IsRoughPart.ne_zero {q n w : ℕ} (h : q.IsRoughPart n w) (hn : n ≠ 0) : w ≠ 0

theorem Nat.IsRoughPart.eq_prod_filter {q n w : ℕ} (h : q.IsRoughPart n w) (hn : n ≠ 0) : w = (List.filter (fun (x : ℕ) => decide (q ≤ x)) n.primeFactorsList).prod

The part of n ≠ 0 at the primes from q on is the product of its prime factors from q on, with multiplicity.

theorem Nat.IsRoughPart.succ {p n v m : ℕ} (h : p.IsRoughPart n (p ^ v * m)) (hp : Prime p) (hpm : ¬p ∣ m) : (p + 1).IsRoughPart n m

Dividing the part p ^ v m, p ∤ m, of n at the primes from the prime p on by p ^ v leaves the part of n at the primes from p + 1 on.

theorem Nat.IsRoughPart.of_le_of_forall {q q' n w : ℕ} (h : q.IsRoughPart n w) (hqq : q ≤ q') (hno : ∀ (p : ℕ), Prime p → q ≤ p → q' ≤ p) : q'.IsRoughPart n w

The part of n at the primes from q on is its part from q' ≥ q on when no prime lies between them.