English
The sequence u: N→N has bounded successive differences growth controlled by a fixed C: for all n, u(n+2)−u(n+1) ≤ C·(u(n+1)−u(n)).
Русский
Последовательность u: ℕ → ℕ удовлетворяет ограничению роста последовательных разностей: ∀n, u(n+2)−u(n+1) ≤ C·(u(n+1)−u(n)).
LaTeX
$$$\\operatorname{SuccDiffBounded}(C,u):=\\forall n \\in \\mathbb{N},\\; u(n+2)-u(n+1) \\le C\\cdot (u(n+1)-u(n))$$$
Lean4
/-- A sequence `u` has the property that its ratio of successive differences is bounded
when there is a positive real number `C` such that, for all n ∈ ℕ,
(u (n + 2) - u (n + 1)) ≤ C * (u (n + 1) - u n)
-/
def SuccDiffBounded (C : ℕ) (u : ℕ → ℕ) : Prop :=
∀ n : ℕ, u (n + 2) - u (n + 1) ≤ C • (u (n + 1) - u n)
