English
If the Cauchy property holds for the sequence of partial sums of g over ranges, and ‖f(i)‖ ≤ g(i) then the same holds for f over ranges.
Русский
Если для диапазона частичных сумм функций g∶ℕ→E выполняется свойство Коши, и ‖f(i)‖ ≤ g(i), то то же верно и для f по диапазонам.
LaTeX
$$$\\bigl(\\text{CauchySeq } n \\mapsto \\sum_{i\\in \\text{range } n} g(i)\\bigr) \\land \\bigl(\\forall i, \\|f(i)\\| \\le g(i)\\bigr) \\Rightarrow \\text{CauchySeq } n \\mapsto \\sum_{i\\in \\text{range } n} f(i)$$$
Lean4
/-- A version of the **direct comparison test** for conditionally convergent series.
See `cauchySeq_finset_of_norm_bounded` for the same statement about absolutely convergent ones. -/
theorem cauchySeq_range_of_norm_bounded {f : ℕ → E} {g : ℕ → ℝ} (hg : CauchySeq fun n => ∑ i ∈ range n, g i)
(hf : ∀ i, ‖f i‖ ≤ g i) : CauchySeq fun n => ∑ i ∈ range n, f i :=
by
refine Metric.cauchySeq_iff'.2 fun ε hε => ?_
refine (Metric.cauchySeq_iff'.1 hg ε hε).imp fun N hg n hn => ?_
specialize hg n hn
rw [dist_eq_norm, ← sum_Ico_eq_sub _ hn] at hg ⊢
calc
‖∑ k ∈ Ico N n, f k‖ ≤ ∑ k ∈ _, ‖f k‖ := norm_sum_le _ _
_ ≤ ∑ k ∈ _, g k := (sum_le_sum fun x _ => hf x)
_ ≤ ‖∑ k ∈ _, g k‖ := (le_abs_self _)
_ < ε := hg
