English
If the ratio ∥f(n+1)∥ / ∥f(n)∥ tends to l < 1 and f(n) ≠ 0 eventually, then f is summable.
Русский
Если предел отношения норм стремится к l < 1 и в конце не равно нулю, то сумма сходится.
LaTeX
$$$\forall {f : \mathbb{N} \to E} [\text{NormedAddCommGroup } E] {l : \mathbb{R}} (hl: l < 1) (hf: ∀ᶠ n in atTop, f(n) ≠ 0) (h: Tendsto (\lambda n, ∥f(n+1)∥ / ∥f(n)∥) atTop (nhds l)) : Summable f$$$
Lean4
theorem not_summable_of_ratio_test_tendsto_gt_one {α : Type*} [SeminormedAddCommGroup α] {f : ℕ → α} {l : ℝ}
(hl : 1 < l) (h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)) : ¬Summable f :=
by
have key : ∀ᶠ n in atTop, ‖f n‖ ≠ 0 :=
by
filter_upwards [h.eventually_const_le hl] with _ hn hc
rw [hc, _root_.div_zero] at hn
linarith
rcases exists_between hl with ⟨r, hr₀, hr₁⟩
refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently ?_
filter_upwards [h.eventually_const_le hr₁, key] with _ _ h₁
rwa [← le_div_iff₀ (lt_of_le_of_ne (norm_nonneg _) h₁.symm)]
