English
Let f: ℕ → ℝ with f(n) ≥ 0 for all n, and assume that the partial sums ∑_{i< n} f(i) are bounded above by c for every n. Then ∑_{n} f(n) is summable (finite).
Русский
Пусть f: ℕ → ℝ удовлетворяет f(n) ≥ 0 и для каждого n частичные суммы ∑_{i< n} f(i) не превосходят c. Тогда ∑_{n≥0} f(n) сходится (суммируема).
LaTeX
$$$\left(\forall n, f(n) \ge 0\right) \land \left(\forall n, \sum_{i=0}^{n-1} f(i) \le c\right) \Rightarrow \text{Summable } f$$$
Lean4
theorem summable_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n) (h : ∀ n, ∑ i ∈ Finset.range n, f i ≤ c) :
Summable f := by
refine (summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_
rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
exact lt_irrefl _ (hn.trans_le (h n))
