geom_lt — Mathlib

English

Under the same hypotheses as geom_lt but with ≤, we have c^n u(0) ≤ u(n).

Русский

При тех же предположениях, но с нестрогим неравенством, имеем c^n u(0) ≤ u(n).

LaTeX

$$$$ c^n \\cdot u(0) \\le u(n) \\quad \\text{for all } n, $$$$

Lean4

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

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