English
The set of k-smooth numbers ≤ N is contained in the image of the map (s,m) ↦ m^2 · (s.prod id), where s ∈ k.primesBelow.powerset and m ∈ {1,2,...,⎣√N⎦}.
Русский
Множество k-гладких чисел ≤ N содержится в образе отображения (s,m) ↦ m^2 · (s.prod id), где s ∈ k.primesBelow.powerset и m ∈ {1,...,⎣√N⎦}.
LaTeX
$$$\mathrm{smoothNumbersUpTo}(N,k) \subseteq \mathrm{image}\left( (s,m) \mapsto m^2 \cdot (s.prod\ id) \right)\left( k.primesBelow.powerset \times \{1,\dots, \lfloor \sqrt{N} \rfloor\} \right)$$$
Lean4
/-- 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 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 + 1)).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, 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, sq_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) _
