lt_geom — Mathlib

English

A variant of the geometric bound that uses a ≤ and lt with appropriate indices to conclude a bound on u(n).

Русский

Вариант геометрического неравенства с использованием ≤ и lt для вывода верхней границы на u(n).

LaTeX

$$$$ \\text{(bounded by geometric progression with } c)$$$$

Lean4

theorem lt_geom {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) {n : ℕ} (hn : 0 < 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_pos_lt_seq_of_lt_of_le hn _ h _
  · simp
  · simp [_root_.pow_succ', mul_assoc, le_refl]

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