Documentation

Mathlib.NumberTheory.SmoothNumbers

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.

primesBelow n is the set of primes less than n as a Finset.

Equations
Instances For
    theorem Nat.mem_primesBelow {k : } {n : } :
    n k.primesBelow n < k Nat.Prime n
    theorem Nat.prime_of_mem_primesBelow {p : } {n : } (h : p n.primesBelow) :
    theorem Nat.lt_of_mem_primesBelow {p : } {n : } (h : p n.primesBelow) :
    p < n
    theorem Nat.primesBelow_succ (n : ) :
    n.succ.primesBelow = if Nat.Prime n then insert n n.primesBelow else n.primesBelow
    theorem Nat.not_mem_primesBelow (n : ) :
    nn.primesBelow

    s-factored numbers #

    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
    Instances For
      theorem Nat.mem_factoredNumbers {s : Finset } {m : } :
      m Nat.factoredNumbers s m 0 pm.primeFactorsList, p s

      Membership in Nat.factoredNumbers n is decidable.

      Equations

      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 pm, Nat.Prime pp mp 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 pp mp s

      m is s-factored if and only if all prime divisors of m are in s.

      The Finset of prime factors of an s-factored number is contained in s.

      theorem Nat.mem_factoredNumbers_of_primeFactors_subset {s : Finset } {m : } (hm : m 0) (hp : m.primeFactors s) :

      If m ≠ 0 and the Finset of prime factors of m is contained in s, then m is s-factored.

      m is s-factored if and only if m ≠ 0 and its Finset of prime factors is contained in s.

      The product of two s-factored numbers is again s-factored.

      theorem Nat.prod_mem_factoredNumbers (s : Finset ) (n : ) :
      (List.filter (fun (x : ) => decide (x s)) n.primeFactorsList).prod Nat.factoredNumbers s

      The product of the prime factors of n that are in s is an s-factored number.

      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_compl {N : } {s : Finset } (h : N.primesBelow 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) :

      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 : ps) (hn : n Nat.factoredNumbers s) :
      p.Coprime 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 : }, m.Coprime nf (m * n) = f m * f n) {s : Finset } {p : } (hp : Nat.Prime p) (hs : ps) (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.

      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.
      Instances For
        @[simp]
        theorem Nat.equivProdNatFactoredNumbers_apply {s : Finset } {p : } {e : } {m : } (hp : Nat.Prime p) (hs : ps) (hm : m Nat.factoredNumbers s) :
        ((Nat.equivProdNatFactoredNumbers hp hs) (e, m, hm)) = p ^ e * m
        @[simp]
        theorem Nat.equivProdNatFactoredNumbers_apply' {s : Finset } {p : } (hp : Nat.Prime p) (hs : ps) (x : × (Nat.factoredNumbers s)) :
        ((Nat.equivProdNatFactoredNumbers hp hs) x) = p ^ x.1 * x.2

        n-smooth numbers #

        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
        • n.smoothNumbers = {m : | m 0 pm.primeFactorsList, p < n}
        Instances For
          theorem Nat.mem_smoothNumbers {n : } {m : } :
          m n.smoothNumbers m 0 pm.primeFactorsList, p < n

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

          theorem Nat.smmoothNumbers_eq_factoredNumbers_primesBelow (n : ) :
          n.smoothNumbers = Nat.factoredNumbers n.primesBelow

          The n-smooth numbers agree with the primesBelow n-factored numbers.

          instance Nat.instDecidablePredMemSetSmoothNumbers (n : ) :
          DecidablePred fun (x : ) => x n.smoothNumbers

          Membership in Nat.smoothNumbers n is decidable.

          Equations
          theorem Nat.mem_smoothNumbers_of_dvd {n : } {m : } {k : } (h : m n.smoothNumbers) (h' : k m) :
          k n.smoothNumbers

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

          theorem Nat.mem_smoothNumbers_iff_forall_le {n : } {m : } :
          m n.smoothNumbers m 0 pm, Nat.Prime pp mp < 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 n.smoothNumbers ∀ (p : ), Nat.Prime pp mp < n

          m is n-smooth if and only if all prime divisors of m are less than n.

          theorem Nat.primeFactors_subset_of_mem_smoothNumbers {m : } {n : } (hms : m n.smoothNumbers) :
          m.primeFactors n.primesBelow

          The Finset of prime factors of an n-smooth number is contained in the Finset of primes below n.

          theorem Nat.mem_smoothNumbers_of_primeFactors_subset {m : } {n : } (hm : m 0) (hp : m.primeFactors Finset.range n) :
          m n.smoothNumbers

          m is an n-smooth number if the Finset of its prime factors consists of numbers < n.

          theorem Nat.mem_smoothNumbers_iff_primeFactors_subset {m : } {n : } :
          m n.smoothNumbers m 0 m.primeFactors n.primesBelow

          m is an n-smooth number if and only if m ≠ 0 and the Finset of its prime factors is contained in the Finset of primes below n

          theorem Nat.ne_zero_of_mem_smoothNumbers {n : } {m : } (h : m n.smoothNumbers) :
          m 0

          Zero is never a smooth number

          theorem Nat.mul_mem_smoothNumbers {m₁ : } {m₂ : } {n : } (hm1 : m₁ n.smoothNumbers) (hm2 : m₂ n.smoothNumbers) :
          m₁ * m₂ n.smoothNumbers

          The product of two n-smooth numbers is an n-smooth number.

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

          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) :
          N.succ.smoothNumbers = N.smoothNumbers

          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.

          theorem Nat.smoothNumbers_mono {N : } {M : } (hNM : N M) :
          N.smoothNumbers M.smoothNumbers
          theorem Nat.mem_smoothNumbers_of_lt {m : } {n : } (hm : 0 < m) (hmn : m < n) :
          m n.smoothNumbers

          All m, 0 < m < n are n-smooth numbers

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

          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 p.smoothNumbers) :
          p.Coprime 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 : }, m.Coprime nf (m * n) = f m * f n) {p : } (hp : Nat.Prime p) (e : ) {m : p.smoothNumbers} :
          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) :
          × p.smoothNumbers p.succ.smoothNumbers

          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
          Instances For
            @[simp]
            theorem Nat.equivProdNatSmoothNumbers_apply {p : } {e : } {m : } (hp : Nat.Prime p) (hm : m p.smoothNumbers) :
            ((Nat.equivProdNatSmoothNumbers hp) (e, m, hm)) = p ^ e * m
            @[simp]
            theorem Nat.equivProdNatSmoothNumbers_apply' {p : } (hp : Nat.Prime p) (x : × p.smoothNumbers) :
            ((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.

            The k-smooth numbers up to and including N as a Finset

            Equations
            Instances For
              theorem Nat.mem_smoothNumbersUpTo {N : } {k : } {n : } :
              n N.smoothNumbersUpTo k n N n k.smoothNumbers

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

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

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

                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)

                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 : ) :
                (N.roughNumbersUpTo k).card pN.succ.primesBelow \ k.primesBelow, 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.