geom_le — Mathlib

English

If u(k+1) < c·u(k) for k < n with c≥0, then u(n) < c^n · u(0).

Русский

Если u(k+1) < c·u(k) для k < n и c ≥ 0, то u(n) < c^n·u(0).

LaTeX

$$$$ u(n) < c^n \\cdot u(0) \\quad \\text{under the given hypotheses.} $$$$

Lean4

theorem geom_le {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (h : ∀ k < n, c * u k ≤ u (k + 1)) : c ^ n * u 0 ≤ u n := by
  apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h <;> simp [_root_.pow_succ', mul_assoc, le_refl]

Похожие утверждения