English
If a sequence f has a Cauchy series of partial sums, then there exists a constant C such that ∥f(n)∥ ≤ C for all n.
Русский
Если частичные суммы сходятся (последовательность Коши), то ∃ константа C, такая что ∥f(n)∥ ≤ C для всех n.
LaTeX
$$$\forall {\alpha} [\text{SeminormedAddCommGroup } \alpha] {f : \mathbb{N} \to \alpha} \\ (\text{CauchySeq } (\lambda n, (\sum_{k< n} f(k)))) \Rightarrow ∃ C, \forall n, ∥f(n)∥ ≤ C$$$
Lean4
theorem summable_of_ratio_norm_eventually_le {α : Type*} [SeminormedAddCommGroup α] [CompleteSpace α] {f : ℕ → α}
{r : ℝ} (hr₁ : r < 1) (h : ∀ᶠ n in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖) : Summable f :=
by
by_cases hr₀ : 0 ≤ r
· rw [eventually_atTop] at h
rcases h with ⟨N, hN⟩
rw [← @summable_nat_add_iff α _ _ _ _ N]
refine
.of_norm_bounded (g := fun n ↦ ‖f N‖ * r ^ n) (Summable.mul_left _ <| summable_geometric_of_lt_one hr₀ hr₁)
fun n ↦ ?_
simp only
conv_rhs => rw [mul_comm, ← zero_add N]
refine le_geom (u := fun n ↦ ‖f (n + N)‖) hr₀ n fun i _ ↦ ?_
convert hN (i + N) (N.le_add_left i) using 3
ac_rfl
· push_neg at hr₀
refine .of_norm_bounded_eventually_nat summable_zero ?_
filter_upwards [h] with _ hn
by_contra! h
exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn <| mul_neg_of_neg_of_pos hr₀ h)
