linearGrowthInf — Mathlib

English

Define the lower linear growth of a sequence u by linearGrowthInf(u) := liminf_{n→∞} u(n)/n. This measures how fast the sequence grows linearly from below.

Русский

Определим нижний линейный рост последовательности u как liminf_{n→∞} u(n)/n. Этот показатель измеряет скороть роста до линейной шкалы.

LaTeX

$$$ \\text{linearGrowthInf} (u) := \\liminf_{n\\to\\infty} \\frac{u(n)}{n} $$$

Lean4

/-- Lower linear growth of a sequence. -/
noncomputable def linearGrowthInf (u : ℕ → R) : R :=
  liminf (fun n ↦ u n / n) atTop

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