English
A refined bound: (roughNumbersUpTo N k).card ≤ N · (N.succ.primesBelow \ k.primesBelow).sum (1/p) as a real bound.
Русский
Улучшенное ограничение: кардинальность roughNumbersUpTo(N,k) ≤ N · ∑_{p ≤ N, p ≥ k} 1/p как вещественное неравенство.
LaTeX
$$$(roughNumbersUpTo(N,k)).card \le N \cdot \Big( (N.succ.primesBelow \ k.primesBelow).\text{sum} \big( \lambda p, (1 : \mathbb{R}) / p \big) \Big)$$$
Lean4
/-- The cardinality of the set of `k`-rough numbers `≤ N` is bounded by `N` times the sum
of `1/p` over the primes `k ≤ p ≤ N`. -/
-- This needs `Mathlib/Analysis/RCLike/Basic.lean`, so we put it here
-- instead of in `Mathlib/NumberTheory/SmoothNumbers.lean`.
theorem roughNumbersUpTo_card_le' (N k : ℕ) :
(roughNumbersUpTo N k).card ≤ N * (N.succ.primesBelow \ k.primesBelow).sum (fun p ↦ (1 : ℝ) / p) :=
by
simp_rw [Finset.mul_sum, mul_one_div]
exact
(Nat.cast_le.mpr <| roughNumbersUpTo_card_le N k).trans <|
cast_sum (R := ℝ) .. ▸ Finset.sum_le_sum fun n _ ↦ cast_div_le
