English
If for a sequence f in a normed additive group, the limit of the ratio ∥f(n+1)∥ / ∥f(n)∥ exists and is less than 1, then f is summable.
Русский
Если предел отношения норм последовательности существует и меньше единицы, то последовательность умеет суммироваться.
LaTeX
$$$\forall {f : \mathbb{N} \to E} [\text{NormedAddCommGroup } E] \; (l : \mathbb{R})\, (hl1: l < 1) (hf : ∀ᶠ n in atTop, ‖f(n+1)‖ ≤ l · ‖f(n)‖) : Summable f$$$
Lean4
theorem summable_of_ratio_test_tendsto_lt_one {α : Type*} [NormedAddCommGroup α] [CompleteSpace α] {f : ℕ → α} {l : ℝ}
(hl₁ : l < 1) (hf : ∀ᶠ n in atTop, f n ≠ 0) (h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)) : Summable f :=
by
rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩
refine summable_of_ratio_norm_eventually_le hr₁ ?_
filter_upwards [h.eventually_le_const hr₀, hf] with _ _ h₁
rwa [← div_le_iff₀ (norm_pos_iff.mpr h₁)]
