expGrowthSup — Mathlib

English

expGrowthSup is the upper exponential growth rate defined as the limsup of log(u(n))/n.

Русский

expGrowthSup задаёт верхний показатель экспоненциального роста, равный limsup(log u(n)/n).

LaTeX

$$$\\text{expGrowthSup}(u) = \\limsup_{n\\to\\infty} \\frac{\\log(u(n))}{n}.$$$

Lean4

/-- Upper exponential growth of a sequence of extended nonnegative real numbers. -/
noncomputable def expGrowthSup (u : ℕ → ℝ≥0∞) : EReal :=
  limsup (fun n ↦ log (u n) / n) atTop

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