Nat.Prime.smoothNumbers_coprime
theorem Nat.Prime.smoothNumbers_coprime : ∀ {p n : ℕ}, p.Prime → n ∈ p.smoothNumbers → p.Coprime n
This theorem states that if `p` is a prime number and `n` is `p`-smooth (meaning that the largest prime factor of `n` is not greater than `p`), then `p` and `n` are coprime. In other words, the greatest common divisor of `p` and `n` is 1. This theorem applies for all natural numbers `p` and `n`.
More concisely: If a prime number `p` divides the product of another number `n` and itself, i.e., `p | (n * p)`, then `p` and `n` are coprime, i.e., `gcd(p, n) = 1`.
|
Nat.smoothNumbersUpTo_card_le
theorem Nat.smoothNumbersUpTo_card_le : ∀ (N k : ℕ), (N.smoothNumbersUpTo k).card ≤ 2 ^ k.primesBelow.card * N.sqrt
The theorem states that for any natural numbers `N` and `k`, the number of `k`-smooth numbers up to and including `N` (a `k`-smooth number is a number whose largest prime factor is less than or equal to `k`) is less than or equal to `2` raised to the power of the number of primes less than `k`, times the square root of `N`. In mathematical terms, this can be written as: the cardinality of the set of `k`-smooth numbers less than or equal to `N` is bounded by `2^π(k-1) * √N`.
More concisely: The number of `k`-smooth numbers up to and including `N` is bounded by `2^π(k) * √N`, where `π(k)` denotes the number of primes less than `k`.
|
Nat.smoothNumbers_compl
theorem Nat.smoothNumbers_compl : ∀ (N : ℕ), N.smoothNumbersᶜ \ {0} ⊆ {n | N ≤ n}
This theorem states that for every natural number `N`, the set of all natural numbers that aren't `N`-smooth (excluding zero) is a subset of the set of all natural numbers `n` that are greater than or equal to `N`. In other words, any non-zero natural number that isn't `N`-smooth must be at least `N`.
More concisely: The set of natural numbers not smooth to a given natural number N is a subset of the natural numbers greater than or equal to N. (Here, "smooth to a given natural number N" refers to numbers having only small prime factors, i.e., not divisible by N except for 1.)
|
Nat.prod_mem_smoothNumbers
theorem Nat.prod_mem_smoothNumbers :
∀ (n N : ℕ), (List.filter (fun x => decide (x < N)) n.factors).prod ∈ N.smoothNumbers
This theorem states that for any two natural numbers `n` and `N`, the product of the prime factors of `n` that are less than `N` belongs to the set of `N`-smooth numbers. The `N`-smooth numbers are the numbers whose largest prime factor is at most `N`. The prime factors of `n` that are less than `N` are obtained by filtering `n`'s factors with the condition that they are less than `N`. The result of this filter operation is a list, and the product of the elements of this list is the number that is claimed to be `N`-smooth.
More concisely: For any natural numbers `n` and `N`, the product of the prime factors of `n` less than `N` is an `N`-smooth number.
|
Nat.pow_mul_mem_smoothNumbers
theorem Nat.pow_mul_mem_smoothNumbers :
∀ {p n : ℕ}, p ≠ 0 → ∀ (e : ℕ), n ∈ p.smoothNumbers → p ^ e * n ∈ p.succ.smoothNumbers
This theorem states that for any positive natural number `p` and any `p`-smooth number `n`, for any natural number `e`, the product `p^e * n` is `(p+1)`-smooth. In mathematical terms, if `n` is a number whose prime factors all less than or equal to `p`, then for any `e`, the product of `p` raised to the power `e` and `n` has all its prime factors less than or equal to `p+1`.
More concisely: For any positive natural number p and p-smooth number n, the product p^e * n is (p+1)-smooth for all natural numbers e.
|
Nat.smoothNumbers_succ
theorem Nat.smoothNumbers_succ : ∀ {N : ℕ}, ¬N.Prime → N.succ.smoothNumbers = N.smoothNumbers
The theorem `Nat.smoothNumbers_succ` states that for any natural number `N`, if `N` is not a prime number, then the sets of `N`-smooth numbers and `(N+1)`-smooth numbers are the same. Here, a number is considered `N`-smooth if its largest prime factor is less than or equal to `N`. This theorem provides an exception to the case when `N` is prime, which is handled separately in `Nat.equivProdNatSmoothNumbers`.
More concisely: If a natural number `N` is not prime, then the sets of `N`-smooth numbers and `(N+1)`-smooth numbers are equal.
|
Nat.mem_smoothNumbers'
theorem Nat.mem_smoothNumbers' : ∀ {n m : ℕ}, m ∈ n.smoothNumbers ↔ ∀ (p : ℕ), p.Prime → p ∣ m → p < n
A natural number `m` is said to be `n`-smooth if and only if all its prime divisors are less than `n`. The theorem `Nat.mem_smoothNumbers'` states this property: for any natural numbers `n` and `m`, `m` is `n`-smooth if and only if, for every prime number `p`, if `p` divides `m`, then `p` is less than `n`.
More concisely: A natural number `m` is `n`-smooth if and only if all its prime divisors are less than `n`.
|
Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers
theorem Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers :
∀ {n k : ℕ}, n ∈ k.smoothNumbers → ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id
This theorem states that for any natural numbers `n` and `k`, if `n` is a `k`-smooth number — that is, if the number `n` can be represented by only using prime factors less than or equal to `k` — then there exists a subset `s` of the primes less than `k` and a natural number `m` such that `n` is equivalent to the square of `m` multiplied by the product of the primes in `s`. The `id` function is used here to denote the identity function, i.e., each element is mapped to itself.
More concisely: For any natural numbers `n` and `k`, if `n` is `k`-smooth, then there exist natural numbers `m` and a subset `s` of primes less than `k`, such that `n = m^2 * (id s).prod`, where `id s` is the identity function on `s` and `prod` denotes their product.
|
Nat.map_prime_pow_mul
theorem Nat.map_prime_pow_mul :
∀ {F : Type u_1} [inst : CommSemiring F] {f : ℕ → F},
(∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
∀ {p : ℕ}, p.Prime → ∀ (e : ℕ) {m : ↑p.smoothNumbers}, f (p ^ e * ↑m) = f (p ^ e) * f ↑m
The theorem `Nat.map_prime_pow_mul` states that, for a given function `f` from natural numbers to a commutative semiring `F`, if this function `f` is multiplicative on coprime arguments (that is, `f(m*n) = f(m)*f(n)` whenever `m` and `n` are coprime), and if `p` is a prime number and `m` is `p`-smooth (meaning that every prime dividing `m` is less than or equal to `p`), then for any natural number `e`, the function `f` evaluated at the product of `p^e` and `m` is equal to the product of `f(p^e)` and `f(m)`. This theorem essentially asserts a certain kind of multiplicativity property of the function `f` under the conditions that the arguments are coprime and `p`-smooth.
More concisely: If `f` is a multiplicative function on coprime arguments and `p` is a prime number such that every prime dividing `m` is less than or equal to `p`, then `f(p^e * m) = f(p^e) * f(m)` for any natural number `e`.
|
Nat.mem_smoothNumbers_of_dvd
theorem Nat.mem_smoothNumbers_of_dvd : ∀ {n m k : ℕ}, m ∈ n.smoothNumbers → k ∣ m → k ∈ n.smoothNumbers
This theorem states that for any natural numbers `n`, `m`, and `k`, if `m` is an `n`-smooth number (a number whose largest prime factor is less than or equal to `n`) and `k` divides `m`, then `k` must also be an `n`-smooth number. In other words, any divisor of an `n`-smooth number is itself `n`-smooth.
More concisely: If `m` is `n`-smooth and `k` divides `m`, then `k` is also `n`-smooth.
|
Nat.roughNumbersUpTo_eq_biUnion
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)
This theorem states that for any two natural numbers `N` and `k`, the set of `k`-rough numbers less than or equal to `N` can be expressed as a combination of sets. More specifically, the set is the union of sets of multiples less than or equal to `N` for each prime number `p` between `k` and `N`. In other words, for each of these primes `p`, it includes all the numbers in the set from `0` to `N` that are divisible by `p`, excluding zero.
More concisely: For any natural number `N` and `k`, the set of `k`-rough numbers less than or equal to `N` is the union of sets of multiples less than or equal to `N` for all primes `p` between `k` and `N`.
|
Nat.smoothNumbersUpTo_subset_image
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)
This theorem states that for any natural numbers `N` and `k`, the set of `k`-smooth numbers less than or equal to `N` is a subset of the set of numbers obtained by the function mapping a pair `(s, m)` to `m` squared times the product of elements in `s` over the cartesian product of the power set of primes less than `k` and the set of natural numbers less than or equal to the square root of `N`, excluding zero. Here, a `k`-smooth number is a number whose prime factors are all less than or equal to `k`. The function `id` is the identity function, indicating that the product does not modify the elements of `s`.
More concisely: For all natural numbers N and k, the set of k-smooth numbers less than or equal to N is included in the set of numbers m obtained by m squared multiplied by the product of elements in the cartesian product of the power set of primes less than k and the set of natural numbers less than or equal to the square root of N, excluding zero. In other words, the set of k-smooth numbers is a subset of {m : sqrt(N) >= m and m = id(s) * (p1^e1 * p2^e2 * ... * pk-1^e(pk-1) | p1,...,pk-1 prime < k and e1,...,ek-1 non-negative integers}.
|
Nat.mem_smoothNumbers_iff_forall_le
theorem Nat.mem_smoothNumbers_iff_forall_le :
∀ {n m : ℕ}, m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ≤ m, p.Prime → p ∣ m → p < n
The theorem `Nat.mem_smoothNumbers_iff_forall_le` states that a natural number `m` is `n`-smooth if and only if `m` is not zero and all of its prime divisors that are less than or equal to `m` are strictly less than `n`. In mathematical terms, for any two natural numbers `n` and `m`, `m` belongs to the set of `n`-smooth numbers if and only if `m` is not zero, and for any prime number `p` that is less than or equal to `m`, if `p` divides `m` then `p` is less than `n`.
More concisely: A natural number `m` is `n`-smooth if and only if it's non-zero and all prime divisors `p` of `m` satisfy `p < n`.
|
Nat.roughNumbersUpTo_card_le
theorem Nat.roughNumbersUpTo_card_le :
∀ (N k : ℕ), (N.roughNumbersUpTo k).card ≤ (N.succ.primesBelow \ k.primesBelow).sum fun p => N / p
This theorem states that for any natural numbers `N` and `k`, the cardinality (size) of the set of `k`-rough numbers less than or equal to `N` is bounded by the sum of the integer division `⌊N/p⌋` over all prime numbers `p` such that `k ≤ p ≤ N`. Here, a `k`-rough number is a number whose smallest prime factor is greater than or equal to `k`.
More concisely: The number of `k`-rough numbers less than or equal to `N` is bounded by the sum of the integer divisors of `N` in the interval `[k, N]`.
|