English
Let u be a sequence of real numbers, and let c be a nonnegative real number. If for a fixed n the inequality u(k+1) ≤ c · u(k) holds for every k < n, then u(n) ≤ c^n · u(0).
Русский
Пусть u : ℕ → ℝ — последовательность, a c ∈ ℝ с 0 ≤ c. Если для заданного n выполняется u(k+1) ≤ c · u(k) для всех k < n, то u(n) ≤ c^n · u(0).
LaTeX
$$$\\\\forall u: \\\\mathbb{N} \\\\to \\\\mathbb{R}, \\\\forall c \\\\in \\\\mathbb{R}, 0 \\\\le c \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{N}, \\\\bigl(\\\\forall k < n, \\\\ u(k+1) \\\\le c \\\\ u(k)\\\\bigr) \\\\Rightarrow \\\\ u(n) \\\\le c^n \\\\ u(0).$$$
Lean4
theorem le_geom {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (h : ∀ k < n, u (k + 1) ≤ c * u k) : u n ≤ c ^ n * u 0 := by
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ h _ <;> simp [_root_.pow_succ', mul_assoc, le_refl]
