Rough numbers

DefinitionRough numbers#✓fully proved

Let \(n\) and \(k\) be natural numbers. Then \(n\) is \(k\)-rough if \(n \neq 0\) and every prime \(p\) dividing \(n\) satisfies \(k < p\); that is, \(n\) is positive and has no prime factor at most \(k\).

In particular \(0\) is not rough, and \(1\) is \(k\)-rough for every \(k\) by vacuity.

def IsRough (n k : ℕ) : Prop :=
  n ≠ 0 ∧ ∀ p : ℕ, p.Prime → p ∣ n → k < p

Sources

• Pandey, arXiv 2307.14890v1, footnote definition (hybrid.tex line 91).

Used by 13

Used byOnly \(1\) is rough and smooth at the same bound · Characterization of rough numbers · A prime is rough exactly above the bound · Roughness through the list of prime factors · A product is rough exactly when both factors are · The number \(1\) is rough · Prime divisors of a rough number exceed the bound · Rough numbers other than \(1\) lie in Mathlib's rough numbers up to a bound · Products of rough numbers are rough · Rough numbers are nonzero · Divisors of rough numbers are rough · Roughness is antitone in the bound · Rough numbers are positive

TheoremCharacterization of rough numbers#✓fully proved

For natural numbers \(n\) and \(k\), \(n\) is \(k\)-rough if and only if \(n \neq 0\) and every prime \(p\) dividing \(n\) satisfies \(k < p\).

theorem isRough_iff {n k : ℕ} :
    n.IsRough k ↔ n ≠ 0 ∧ ∀ p : ℕ, p.Prime → p ∣ n → k < p

Uses 1

Statement usesRough numbers

TheoremRough numbers are nonzero#✓fully proved

For every natural number \(k\), every \(k\)-rough natural number \(n\) satisfies \(n \ne 0\).

theorem IsRough.ne_zero {n k : ℕ} (h : n.IsRough k) : n ≠ 0

Uses 1 · Used by 6

Statement usesRough numbers

Used byOnly \(1\) is rough and smooth at the same bound · Roughness through the list of prime factors · A product is rough exactly when both factors are · Rough numbers other than \(1\) lie in Mathlib's rough numbers up to a bound · Roughness is antitone in the bound · Rough numbers are positive

TheoremRough numbers are positive#✓fully proved

For every natural number \(k\), every \(k\)-rough natural number \(n\) satisfies \(n > 0\).

theorem IsRough.pos {n k : ℕ} (h : n.IsRough k) : 0 < n

Uses 2

Statement usesRough numbers

Proof usesRough numbers are nonzero

TheoremPrime divisors of a rough number exceed the bound#✓fully proved

Let \(n\), \(k\) and \(p\) be natural numbers. If \(n\) is \(k\)-rough and \(p\) is a prime dividing \(n\), then \(k < p\).

theorem IsRough.lt_of_prime_dvd {n k p : ℕ} (h : n.IsRough k) (hp : p.Prime)
    (hdvd : p ∣ n) : k < p

Uses 1 · Used by 6

Statement usesRough numbers

Used byOnly \(1\) is rough and smooth at the same bound · A prime is rough exactly above the bound · Roughness through the list of prime factors · A product is rough exactly when both factors are · Divisors of rough numbers are rough · Roughness is antitone in the bound

TheoremRoughness through the list of prime factors#✓fully proved

For natural numbers \(n\) and \(k\), \(n\) is \(k\)-rough if and only if \(n \neq 0\) and every prime in the list of prime factors of \(n\) (with multiplicity) is greater than \(k\).

theorem isRough_iff_primeFactorsList {n k : ℕ} :
    n.IsRough k ↔ n ≠ 0 ∧ ∀ p ∈ primeFactorsList n, k < p

Uses 3

Statement usesRough numbers

Proof usesPrime divisors of a rough number exceed the bound · Rough numbers are nonzero

TheoremThe number \(1\) is rough#✓fully proved

For every natural number \(k\), the number \(1\) is \(k\)-rough.

This holds vacuously, since \(1\) has no prime divisors.

theorem isRough_one (k : ℕ) : (1 : ℕ).IsRough k

Uses 1

Statement usesRough numbers

TheoremA prime is rough exactly above the bound#✓fully proved

For natural numbers \(p\) and \(k\) with \(p\) prime, \(p\) is \(k\)-rough if and only if \(k < p\).

theorem Prime.isRough_iff {p k : ℕ} (hp : p.Prime) : p.IsRough k ↔ k < p

Uses 2

Statement usesRough numbers

Proof usesPrime divisors of a rough number exceed the bound

TheoremDivisors of rough numbers are rough#✓fully proved

Let \(k\) be a natural number. If a natural number \(m\) is \(k\)-rough and \(d\) is a nonzero divisor of \(m\), then \(d\) is \(k\)-rough.

theorem IsRough.of_dvd {m d k : ℕ} (h : m.IsRough k) (hdvd : d ∣ m) (hd : d ≠ 0) :
    d.IsRough k

Uses 2 · Used by 1

Statement usesRough numbers

Proof usesPrime divisors of a rough number exceed the bound

Used byA product is rough exactly when both factors are

TheoremA product is rough exactly when both factors are#✓fully proved

For natural numbers \(m\), \(n\) and \(k\), the product \(mn\) is \(k\)-rough if and only if both \(m\) and \(n\) are \(k\)-rough.

theorem isRough_mul {m n k : ℕ} : (m * n).IsRough k ↔ m.IsRough k ∧ n.IsRough k

Uses 4 · Used by 1

Statement usesRough numbers

Proof usesPrime divisors of a rough number exceed the bound · Rough numbers are nonzero · Divisors of rough numbers are rough

Used byProducts of rough numbers are rough

TheoremProducts of rough numbers are rough#✓fully proved

For natural numbers \(m\), \(n\) and \(k\), if \(m\) and \(n\) are both \(k\)-rough, then \(mn\) is \(k\)-rough.

theorem IsRough.mul {m n k : ℕ} (hm : m.IsRough k) (hn : n.IsRough k) :
    (m * n).IsRough k

Uses 2

Statement usesRough numbers

Proof usesA product is rough exactly when both factors are

TheoremRoughness is antitone in the bound#✓fully proved

Let \(k\) and \(l\) be natural numbers with \(l \le k\). Every \(k\)-rough natural number is \(l\)-rough.

theorem IsRough.of_le {n k l : ℕ} (h : n.IsRough k) (hle : l ≤ k) : n.IsRough l

Uses 3

Statement usesRough numbers

Proof usesPrime divisors of a rough number exceed the bound · Rough numbers are nonzero

TheoremOnly \(1\) is rough and smooth at the same bound#✓fully proved

Let \(n\) and \(k\) be natural numbers. If \(n\) is \(k\)-rough and \(n\) is positive with every prime factor less than \(k + 1\), then \(n = 1\).

theorem IsRough.eq_one_of_mem_smoothNumbers {n k : ℕ}
    (hrough : n.IsRough k) (hsmooth : n ∈ smoothNumbers (k + 1)) : n = 1

Uses 3 · Used by 1

Statement usesRough numbers

Proof usesPrime divisors of a rough number exceed the bound · Rough numbers are nonzero

Used byRough numbers other than \(1\) lie in Mathlib's rough numbers up to a bound

TheoremRough numbers other than \(1\) lie in Mathlib's rough numbers up to a bound#✓fully proved

Let \(n\), \(N\) and \(k\) be natural numbers. If \(n\) is \(k\)-rough, \(n \le N\) and \(n \ne 1\), then \(n\) belongs to the set of natural numbers \(m\) with \(1 \le m \le N\) that are not \((k+1)\)-smooth, where \(m\) is \((k+1)\)-smooth when \(m > 0\) and every prime factor of \(m\) is less than \(k + 1\); for \(m \ge 1\), not being \((k+1)\)-smooth means having a prime factor \(p \ge k + 1\).

This set is Mathlib's set of rough numbers up to \(N\) at bound \(k + 1\). It asks only for some prime factor \(p \ge k + 1\), while \(k\)-roughness asks that every prime factor exceed \(k\).

theorem IsRough.mem_roughNumbersUpTo {n N k : ℕ}
    (h : n.IsRough k) (hle : n ≤ N) (hn1 : n ≠ 1) :
    n ∈ roughNumbersUpTo N (k + 1)

Uses 3

Statement usesRough numbers

Proof usesOnly \(1\) is rough and smooth at the same bound · Rough numbers are nonzero

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.