English
If a sequence v satisfies v(n+1) ≥ c · v(n) with c > 1 and the initial term v(0) > 0, then the sequence tends to +∞.
Русский
Если последовательность v удовлетворяет v(n+1) ≥ c · v(n) для всех n, причём c > 1 и v(0) > 0, то v(n) расходится к +∞.
LaTeX
$$$\\\\forall v: \\\\mathbb{N} \\\\to \\\\mathbb{R}, \\\\forall c \\\\in \\\\mathbb{R}, (0 < v(0)) \\\\wedge (1 < c) \\\\wedge (\\\\forall n, c \\\\cdot v(n) \\\\le v(n+1)) \\\\Rightarrow \\\\ operatorname{Tendsto} \\\\ v \\\\ atTop \\\\ operatorname{atTop}.$$$
Lean4
/-- If a sequence `v` of real numbers satisfies `k * v n ≤ v (n+1)` with `1 < k`,
then it goes to +∞. -/
theorem tendsto_atTop_of_geom_le {v : ℕ → ℝ} {c : ℝ} (h₀ : 0 < v 0) (hc : 1 < c) (hu : ∀ n, c * v n ≤ v (n + 1)) :
Tendsto v atTop atTop :=
(tendsto_atTop_mono fun n ↦ geom_le (zero_le_one.trans hc.le) n fun k _ ↦ hu k) <|
(tendsto_pow_atTop_atTop_of_one_lt hc).atTop_mul_const h₀
