English
If a majorant g is summable and f is eventually dominated by g, then the finite-sum net is Cauchy.
Русский
Если mачорант g суммируем и f в конце концов ограничивается g, то сеть конечных сумм является Коши.
LaTeX
$$$\\text{Summable } g \\land (\\forall^{\\infty} i \\text{ in cofinite}, \\|f(i)\\| \\le g(i)) \\Rightarrow \\text{CauchySeq} \\bigl( s \\mapsto \\sum_{i\\in s} f(i) \\bigr)$$$
Lean4
theorem cauchySeq_finset_of_norm_bounded_eventually {f : ι → E} {g : ι → ℝ} (hg : Summable g)
(h : ∀ᶠ i in cofinite, ‖f i‖ ≤ g i) : CauchySeq fun s => ∑ i ∈ s, f i :=
by
refine cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => ?_
rcases summable_iff_vanishing_norm.1 hg ε hε with ⟨s, hs⟩
classical
refine ⟨s ∪ h.toFinset, fun t ht => ?_⟩
have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
intro i hi
simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff, Classical.not_not] at ht
exact (ht hi).2
calc
‖∑ i ∈ t, f i‖ ≤ ∑ i ∈ t, g i := norm_sum_le_of_le _ this
_ ≤ ‖∑ i ∈ t, g i‖ := (le_abs_self _)
_ < ε := hs _ (ht.mono_right le_sup_left)
