expGrowthInf — Mathlib

English

expGrowthInf is the lower exponential growth rate defined as the liminf of log(u(n))/n.

Русский

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

LaTeX

$$$\\text{expGrowthInf}(u) = \\liminf_{n\\to\\infty} \\frac{\\log(u(n))}{n}.$$$

Lean4

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

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