expGrowthInf_congr — Mathlib

English

If two sequences are eventually equal, their liminf of log over n remains equal after composing with any monotone function.

Русский

Если две последовательности равны после некоторого момента, их liminf логарифма по n совпадает после композиции с любую монотонную функцию.

LaTeX

$$$u =\\!\\!\\!_{{atTop}} v \\Rightarrow \\liminf \\frac{\\log(u(n))}{n} = \\liminf \\frac{\\log(v(n))}{n}.$$$

Lean4

theorem expGrowthInf_congr (h : u =ᶠ[atTop] v) : expGrowthInf u = expGrowthInf v :=
  liminf_congr (h.mono fun _ uv ↦ uv ▸ rfl)

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