English
If f is Summable with f(0)=0, then for every ε>0 there exists N0 such that for all N≥N0, the norm of the difference between the full sum ∑ f(n) and the partial sum over N.primesBelow-factoredNumbers is less than ε, when selecting primesBelow up to N.
Русский
Если f суммируема, f(0)=0, то для любого ε>0 существует N0, такое что для всех N≥N0 норма разности между полной суммой и частичной суммой по простым до N и соответствующим факторизованным числам меньше ε.
LaTeX
$$$\\exists N_0:\\forall N\\ge N_0:\\left\\|\\sum_{n\\ge0} f(n) - \\sum_{m\\in N\\,\\text{primesBelow-factoredNumbers}} f(m)\\right\\| < \\varepsilon.$$$
Lean4
/-- The following statement says that summing over `s`-factored numbers such that
`s` contains `primesBelow N` for large enough `N` gets us arbitrarily close to the sum
over all natural numbers (assuming `f` is summable and `f 0 = 0`; the latter since
`0` is not `s`-factored). -/
theorem norm_tsum_factoredNumbers_sub_tsum_lt (hsum : Summable f) (hf₀ : f 0 = 0) {ε : ℝ} (εpos : 0 < ε) :
∃ N : ℕ, ∀ s : Finset ℕ, primesBelow N ≤ s → ‖(∑' m : ℕ, f m) - ∑' m : factoredNumbers s, f m‖ < ε :=
by
obtain ⟨N, hN⟩ := summable_iff_nat_tsum_vanishing.mp hsum (Metric.ball 0 ε) <| Metric.ball_mem_nhds 0 εpos
simp_rw [mem_ball_zero_iff] at hN
refine ⟨N, fun s hs ↦ ?_⟩
have := hN _ <| factoredNumbers_compl hs
rwa [← hsum.tsum_subtype_add_tsum_subtype_compl (factoredNumbers s), add_sub_cancel_left,
tsum_eq_tsum_diff_singleton (factoredNumbers s)ᶜ hf₀]
-- Versions of the three lemmas above for `smoothNumbers N`
