English
If l > 1 and the ratio ∥f(n+1)∥ / ∥f(n)∥ tends to l, then f is not summable.
Русский
Если предел отношения норм последовательности больше единицы, то сумма не сходится.
LaTeX
$$$\forall {f : \mathbb{N} \to E} [\text{NormedAddCommGroup } E] \; (l : \mathbb{R})\, (hl : 1 < l) (h : Tendsto (\lambda n, ∥f(n+1)∥ / ∥f(n)∥) atTop (nhds l)) : Not (Summable f)$$$
Lean4
theorem not_summable_of_ratio_norm_eventually_ge {α : Type*} [SeminormedAddCommGroup α] {f : ℕ → α} {r : ℝ} (hr : 1 < r)
(hf : ∃ᶠ n in atTop, ‖f n‖ ≠ 0) (h : ∀ᶠ n in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖) : ¬Summable f :=
by
rw [eventually_atTop] at h
rcases h with ⟨N₀, hN₀⟩
rw [frequently_atTop] at hf
rcases hf N₀ with ⟨N, hNN₀ : N₀ ≤ N, hN⟩
rw [← @summable_nat_add_iff α _ _ _ _ N]
refine mt Summable.tendsto_atTop_zero fun h' ↦ not_tendsto_atTop_of_tendsto_nhds (tendsto_norm_zero.comp h') ?_
convert tendsto_atTop_of_geom_le _ hr _
· refine lt_of_le_of_ne (norm_nonneg _) ?_
intro h''
specialize hN₀ N hNN₀
simp only [comp_apply, zero_add] at h''
exact hN h''.symm
· grind
