feat(NumberTheory.SmoothNumbers): add {smooth|rough}NumbersUpTo and…

… some API (#9240)

This adds definitions of the `k`-smooth numbers up to and including `N` as a `Finset` and of its complement in `{1, ..., N}` plus some API, in particular cardinality bounds. There are also a few additional API lemmas for `Nat.primesBelow` and `Nat.smoothNumbers` (including a decidability instance for membership in the latter).

This is a PR in preparation of the divergence of the sum of the reciprocals of the primes. See [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Sum.20over.201.2Fp.20diverges/near/409835682) on Zulip.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Data/Nat/Factorization/Basic.lean

@@ -866,7 +866,8 @@ theorem prod_pow_prime_padicValNat (n : Nat) (hn : n ≠ 0) (m : Nat) (pr : n <
 
 
 -- TODO: Port lemmas from `Data/Nat/Multiplicity` to here, re-written in terms of `factorization`
-/-- Exactly `n / p` naturals in `[1, n]` are multiples of `p`. -/
+/-- Exactly `n / p` naturals in `[1, n]` are multiples of `p`.
+See `Nat.card_multiples'` for an alternative spelling of the statement.  -/
 theorem card_multiples (n p : ℕ) : card ((Finset.range n).filter fun e => p ∣ e + 1) = n / p := by
   induction' n with n hn
   · simp
@@ -887,4 +888,16 @@ theorem Ioc_filter_dvd_card_eq_div (n p : ℕ) : ((Ioc 0 n).filter fun x => p 
     Finset.mem_filter, mem_Ioc, not_le.2 (lt_add_one n), Nat.succ_eq_add_one]
 #align nat.Ioc_filter_dvd_card_eq_div Nat.Ioc_filter_dvd_card_eq_div
 
+/-- There are exactly `⌊N/n⌋` positive multiples of `n` that are `≤ N`.
+See `Nat.card_multiples` for a "shifted-by-one" version. -/
+lemma card_multiples' (N n : ℕ) :
+    ((Finset.range N.succ).filter (fun k ↦ k ≠ 0 ∧ n ∣ k)).card = N / n := by
+  induction N with
+    | zero => simp
+    | succ N ih =>
+        rw [Finset.range_succ, Finset.filter_insert]
+        by_cases h : n ∣ N.succ
+        · simp [h, succ_div_of_dvd, ih]
+        · simp [h, succ_div_of_not_dvd, ih]
+
 end Nat

Mathlib/NumberTheory/SmoothNumbers.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Stoll
 -/
 import Mathlib.Data.Nat.Factorization.Basic
+import Mathlib.Data.Nat.Squarefree
 
 /-!
 # Smooth numbers
@@ -16,6 +17,11 @@ We also define the finite set `Nat.primesBelow n` to be the set of prime numbers
 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.
+
+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`.
 -/
 
 namespace Nat
@@ -27,6 +33,9 @@ def primesBelow (n : ℕ) : Finset ℕ := (Finset.range n).filter (fun p ↦ p.P
 lemma primesBelow_zero : primesBelow 0 = ∅ := by
   rw [primesBelow, Finset.range_zero, Finset.filter_empty]
 
+lemma mem_primesBelow {k n : ℕ} :
+    n ∈ primesBelow k ↔ n < k ∧ n.Prime := by simp [primesBelow]
+
 lemma prime_of_mem_primesBelow {p n : ℕ} (h : p ∈ n.primesBelow) : p.Prime :=
   (Finset.mem_filter.mp h).2
 
@@ -47,14 +56,37 @@ def smoothNumbers (n : ℕ) : Set ℕ := {m | m ≠ 0 ∧ ∀ p ∈ factors m, p
 lemma mem_smoothNumbers {n m : ℕ} : m ∈ smoothNumbers n ↔ m ≠ 0 ∧ ∀ p ∈ factors m, p < n :=
   Iff.rfl
 
+/-- Membership in `Nat.smoothNumbers n` is decidable. -/
+instance (n : ℕ) : DecidablePred (· ∈ smoothNumbers n) :=
+  inferInstanceAs <| DecidablePred fun x ↦ x ∈ {m | m ≠ 0 ∧ ∀ p ∈ factors m, p < n}
+
+/-- A number that divides an `n`-smooth number is itself `n`-smooth. -/
+lemma mem_smoothNumbers_of_dvd {n m k : ℕ} (h : m ∈ smoothNumbers n) (h' : k ∣ m) (hk : k ≠ 0) :
+    k ∈ smoothNumbers n := by
+  rw [mem_smoothNumbers] at h ⊢
+  obtain ⟨h₁, h₂⟩ := h
+  refine ⟨hk, fun p hp ↦ h₂ p ?_⟩
+  rw [mem_factors <| by assumption] at hp ⊢
+  exact ⟨hp.1, hp.2.trans h'⟩
+
+/-- `m` is `n`-smooth if and only if `m` is nonzero and all prime divisors `≤ m` of `m`
+are less than `n`. -/
+lemma mem_smoothNumbers_iff_forall_le  {n m : ℕ} :
+    m ∈ smoothNumbers n ↔ m ≠ 0 ∧ ∀ p ≤ m, p.Prime → p ∣ m → p < n := by
+  simp_rw [mem_smoothNumbers, mem_factors']
+  exact ⟨fun ⟨H₀, H₁⟩ ↦ ⟨H₀, fun p _ hp₂ hp₃ ↦ H₁ p ⟨hp₂, hp₃, H₀⟩⟩,
+    fun ⟨H₀, H₁⟩ ↦
+      ⟨H₀, fun p ⟨hp₁, hp₂, hp₃⟩ ↦ H₁ p (Nat.le_of_dvd (Nat.pos_of_ne_zero hp₃) hp₂) hp₁ hp₂⟩⟩
+
 /-- `m` is `n`-smooth if and only if all prime divisors of `m` are less than `n`. -/
 lemma mem_smoothNumbers' {n m : ℕ} : m ∈ smoothNumbers n ↔ ∀ p, p.Prime → p ∣ m → p < n := by
-  rw [mem_smoothNumbers]
-  refine ⟨fun H p hp h ↦ H.2 p <| (mem_factors_iff_dvd H.1 hp).mpr h,
-          fun H ↦ ⟨?_, fun p hp ↦ H p (prime_of_mem_factors hp) (dvd_of_mem_factors hp)⟩⟩
-  rintro rfl
   obtain ⟨p, hp₁, hp₂⟩ := exists_infinite_primes n
-  exact ((H p hp₂ <| dvd_zero _).trans_le hp₁).false
+  rw [mem_smoothNumbers_iff_forall_le]
+  exact ⟨fun ⟨H₀, H₁⟩ ↦ fun p hp₁ hp₂ ↦ H₁ p (Nat.le_of_dvd (Nat.pos_of_ne_zero H₀) hp₂) hp₁ hp₂,
+         fun H ↦ ⟨fun h ↦ ((H p hp₂ <| h.symm ▸ dvd_zero p).trans_le hp₁).false, fun p _ ↦ H p⟩⟩
+
+lemma ne_zero_of_mem_smoothNumbers {n m : ℕ} (h : m ∈ smoothNumbers n) : m ≠ 0 :=
+  (mem_smoothNumbers_iff_forall_le.mp h).1
 
 @[simp]
 lemma smoothNumbers_zero : smoothNumbers 0 = {1} := by
@@ -166,4 +198,97 @@ lemma equivProdNatSmoothNumbers_apply {p e m : ℕ} (hp: p.Prime) (hm : m ∈ p.
 lemma equivProdNatSmoothNumbers_apply' {p : ℕ} (hp: p.Prime) (x : ℕ × p.smoothNumbers) :
     equivProdNatSmoothNumbers hp x = p ^ x.1 * x.2 := rfl
 
+/-- The `k`-smooth numbers up to and including `N` as a `Finset` -/
+def smoothNumbersUpTo (N k : ℕ) : Finset ℕ :=
+    (Finset.range N.succ).filter (· ∈ smoothNumbers k)
+
+lemma mem_smoothNumbersUpTo {N k n : ℕ} :
+    n ∈ smoothNumbersUpTo N k ↔ n ≤ N ∧ n ∈ smoothNumbers k := by
+  simp [smoothNumbersUpTo, lt_succ]
+
+/-- The positive non-`k`-smooth (so "`k`-rough") numbers up to and including `N` as a `Finset` -/
+def roughNumbersUpTo (N k : ℕ) : Finset ℕ :=
+    (Finset.range N.succ).filter (fun n ↦ n ≠ 0 ∧ n ∉ smoothNumbers k)
+
+lemma smoothNumbersUpTo_card_add_roughNumbersUpTo_card (N k : ℕ) :
+    (smoothNumbersUpTo N k).card + (roughNumbersUpTo N k).card = N := by
+  rw [smoothNumbersUpTo, roughNumbersUpTo,
+    ← Finset.card_union_eq <| Finset.disjoint_filter.mpr fun n _ hn₂ h ↦ h.2 hn₂,
+    Finset.filter_union_right]
+  suffices : Finset.card (Finset.filter (fun x ↦ x ≠ 0) (Finset.range (succ N))) = N
+  · convert this with n
+    have hn : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
+    tauto
+  · rw [Finset.filter_ne', Finset.card_erase_of_mem <| Finset.mem_range_succ_iff.mpr <| zero_le N]
+    simp
+
+/-- A `k`-smooth number can be written as a square times a product of distinct primes `< k`. -/
+lemma eq_prod_primes_mul_sq_of_mem_smoothNumbers {n k : ℕ} (h : n ∈ smoothNumbers k) :
+    ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * (s.prod id) := by
+  obtain ⟨l, m, H₁, H₂⟩ := sq_mul_squarefree n
+  have hl : l ∈ smoothNumbers k :=
+    mem_smoothNumbers_of_dvd h (Dvd.intro_left (m ^ 2) H₁) <| Squarefree.ne_zero H₂
+  refine ⟨l.factors.toFinset, ?_,  m, ?_⟩
+  · simp only [toFinset_factors, Finset.mem_powerset]
+    refine fun p hp ↦ mem_primesBelow.mpr ⟨?_, (mem_primeFactors.mp hp).1⟩
+    rw [mem_primeFactors] at hp
+    exact mem_smoothNumbers'.mp hl p hp.1 hp.2.1
+  rw [← H₁]
+  congr
+  simp only [toFinset_factors]
+  exact (prod_primeFactors_of_squarefree H₂).symm
+
+/-- 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`. -/
+lemma smoothNumbersUpTo_subset_image (N k : ℕ) :
+    smoothNumbersUpTo N k ⊆ Finset.image (fun (s, m) ↦ m ^ 2 * (s.prod id))
+      (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0) := by
+  intro n hn
+  obtain ⟨hn₁, hn₂⟩ := mem_smoothNumbersUpTo.mp hn
+  obtain ⟨s, hs, m, hm⟩ := eq_prod_primes_mul_sq_of_mem_smoothNumbers hn₂
+  simp only [id_eq, Finset.mem_range, zero_lt_succ, not_true_eq_false, Finset.mem_image,
+    Finset.mem_product, Finset.mem_powerset, Finset.mem_erase, Prod.exists]
+  refine ⟨s, m, ⟨Finset.mem_powerset.mp hs, ?_, ?_⟩, hm.symm⟩
+  · have := hm ▸ ne_zero_of_mem_smoothNumbers hn₂
+    simp only [ne_eq, _root_.mul_eq_zero, zero_lt_two, pow_eq_zero_iff, not_or] at this
+    exact this.1
+  · rw [lt_succ, le_sqrt']
+    refine LE.le.trans ?_ (hm ▸ hn₁)
+    nth_rw 1 [← mul_one (m ^ 2)]
+    exact mul_le_mul_left' (Finset.one_le_prod' fun p hp ↦
+      (prime_of_mem_primesBelow <| Finset.mem_powerset.mp hs hp).one_lt.le) _
+
+/-- The cardinality of the set of `k`-smooth numbers `≤ N` is bounded by `2^π(k-1) * √N`. -/
+lemma smoothNumbersUpTo_card_le (N k : ℕ) :
+    (smoothNumbersUpTo N k).card ≤ 2 ^ k.primesBelow.card * N.sqrt := by
+  convert (Finset.card_le_card <| smoothNumbersUpTo_subset_image N k).trans <|
+    Finset.card_image_le
+  simp
+
+/-- The set of `k`-rough numbers `≤ N` can be written as the union of the sets of multiples `≤ N`
+of primes `k ≤ p ≤ N`. -/
+lemma roughNumbersUpTo_eq_biUnion (N k) :
+    roughNumbersUpTo N k =
+      (N.succ.primesBelow \ k.primesBelow).biUnion
+        fun p ↦ (Finset.range N.succ).filter (fun m ↦ m ≠ 0 ∧ p ∣ m) := by
+  ext m
+  simp only [roughNumbersUpTo, mem_smoothNumbers_iff_forall_le, not_and, not_forall,
+    not_lt, exists_prop, exists_and_left, Finset.mem_range, not_le, Finset.mem_filter,
+    Finset.filter_congr_decidable, Finset.mem_biUnion, Finset.mem_sdiff, mem_primesBelow,
+    show ∀ P Q : Prop, P ∧ (P → Q) ↔ P ∧ Q by tauto]
+  simp_rw [← exists_and_left, ← not_lt]
+  refine exists_congr fun p ↦ ?_
+  have H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ :=
+    fun h₁ h₂ h₃ ↦ (le_of_dvd (Nat.pos_of_ne_zero h₁) h₂).trans_lt h₃
+  have H₂ : m ≠ 0 → p ∣ m → ¬ m < p :=
+    fun h₁ h₂ ↦ not_lt.mpr <| le_of_dvd (Nat.pos_of_ne_zero h₁) h₂
+  tauto
+
+/-- The cardinality of the set of `k`-rough numbers `≤ N` is bounded by the sum of `⌊N/p⌋`
+over the primes `k ≤ p ≤ N`. -/
+lemma roughNumbersUpTo_card_le (N k : ℕ) :
+    (roughNumbersUpTo N k).card ≤ (N.succ.primesBelow \ k.primesBelow).sum (fun p ↦ N / p) := by
+  rw [roughNumbersUpTo_eq_biUnion]
+  exact Finset.card_biUnion_le.trans <| Finset.sum_le_sum fun p _ ↦ (card_multiples' N p).le
+
 end Nat