English
The cardinality of roughNumbersUpTo(N,k) is bounded by the sum over primes p in ((N+1).primesBelow \ k.primesBelow) of floor(N/p).
Русский
Кардинальность roughNumbersUpTo(N,k) ограничена суммой по простым p в ((N+1).primesBelow \ k.primesBelow) от ⌊N/p⌋.
LaTeX
$$$\#(\mathrm{roughNumbersUpTo}(N,k)) \le \sum_{p \in ((N+1).primesBelow \ k.primesBelow)} \left\lfloor \dfrac{N}{p} \right\rfloor$$$
Lean4
/-- The cardinality of the set of `k`-rough numbers `≤ N` is bounded by the sum of `⌊N/p⌋`
over the primes `k ≤ p ≤ N`. -/
theorem roughNumbersUpTo_card_le (N k : ℕ) :
#(roughNumbersUpTo N k) ≤ ((N + 1).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
