linearGrowthSup — Mathlib

English

Define the upper linear growth of a sequence u by linearGrowthSup(u) := limsup_{n→∞} u(n)/n. This measures the maximal linear growth rate.

Русский

Определим верхний линейный рост последовательности u как limsup_{n→∞} u(n)/n. Это измеряет максимальную скорость линейного роста.

LaTeX

$$$ \\text{linearGrowthSup} (u) := \\limsup_{n\\to\\infty} \\frac{u(n)}{n} $$$

Lean4

/-- Upper linear growth of a sequence. -/
noncomputable def linearGrowthSup (u : ℕ → R) : R :=
  limsup (fun n ↦ u n / n) atTop

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