English
If f : ℕ → R is a summable sequence in a normed commutative ring R and f(0) = 0, then the tail of the series over smooth or factored numbers can be made arbitrarily small; in particular, the norm of the difference between the full sum and the partial sum over a finite family tends to 0 as the finite family grows.
Русский
Пусть f: ℕ → R — последовательность в нормированном кольце R, суммируема и f(0)=0. Тогда разность между суммой по всем числам и суммой по некоторым ограниченным множителям можно сделать сколь угодно малой по мере роста множества. В частности, норма этой разности стремится к нулю при увеличении множества.
LaTeX
$$$\\text{Summable}(f) \\Rightarrow \\exists N_0\\,\\forall N\\ge N_0:\\|\\sum_{n\\ge0} f(n)-\\sum_{m\\in N\\text{smoothNumbers}} f(m)\\|<\\varepsilon.$$$
Lean4
/-- If `f` is multiplicative and summable, then its values at natural numbers `> 1`
have norm strictly less than `1`. -/
theorem norm_lt_one {F : Type*} [NormedDivisionRing F] [CompleteSpace F] {f : ℕ →* F} (hsum : Summable f) {p : ℕ}
(hp : 1 < p) : ‖f p‖ < 1 := by
refine summable_geometric_iff_norm_lt_one.mp ?_
simp_rw [← map_pow]
exact hsum.comp_injective <| Nat.pow_right_injective hp
