English
A version of norm approximation: there exists N0 such that for all N≥N0, the norm of the difference between the total tsum and the tsum over s-factoredNumbers is less than a given ε, provided s contains primesBelow N.
Русский
Существует N0, такое что для всех N≥N0 норма разности между полной суммой и суммой по s-перефакторизованным числам меньше заданной ε при условии, что s содержит primesBelow N.
LaTeX
$$$\\exists N_0:\\forall N\\ge N_0:\\|\\sum_{m\\ge0} f(m) - \\sum_{m\\in \\mathrm{factoredNumbers}(s)} f(m)\\| < \\varepsilon.$$$
Lean4
/-- The following statement says that summing over `N`-smooth numbers
for large enough `N` gets us arbitrarily close to the sum over all natural numbers
(assuming `f` is norm-summable and `f 0 = 0`; the latter since `0` is not smooth). -/
theorem norm_tsum_smoothNumbers_sub_tsum_lt (hsum : Summable f) (hf₀ : f 0 = 0) {ε : ℝ} (εpos : 0 < ε) :
∃ N₀ : ℕ, ∀ N ≥ N₀, ‖(∑' m : ℕ, f m) - ∑' m : N.smoothNumbers, f m‖ < ε :=
by
conv => enter [1, N₀, N]; rw [smoothNumbers_eq_factoredNumbers]
obtain ⟨N₀, hN₀⟩ := norm_tsum_factoredNumbers_sub_tsum_lt hsum hf₀ εpos
refine ⟨N₀, fun N hN ↦ hN₀ (range N) fun p hp ↦ ?_⟩
exact mem_range.mpr <| (lt_of_mem_primesBelow hp).trans_le hN
