English
For all N,k, the cardinality of smoothNumbersUpTo(N,k) is bounded by 2^{π(k-1)} · √N.
Русский
Для всех N,k кардинальность множества smoothNumbersUpTo(N,k) не превышает 2^{π(k-1)} · √N.
LaTeX
$$$\#\big( \mathrm{smoothNumbersUpTo}(N,k) \big) \le 2^{\#k.primesBelow} \cdot N^{1/2}$$$
Lean4
/-- The cardinality of the set of `k`-smooth numbers `≤ N` is bounded by `2^π(k-1) * √N`. -/
theorem smoothNumbersUpTo_card_le (N k : ℕ) : #(smoothNumbersUpTo N k) ≤ 2 ^ #k.primesBelow * N.sqrt :=
by
convert (Finset.card_le_card <| smoothNumbersUpTo_subset_image N k).trans <| Finset.card_image_le
simp only [Finset.card_product, Finset.card_powerset, Finset.mem_range, zero_lt_succ, Finset.card_erase_of_mem,
Finset.card_range, succ_sub_succ_eq_sub, tsub_zero]
