expGrowthSup_congr — Mathlib

English

If two sequences are eventually equal, their limsup of log over n coincide.

Русский

Если две последовательности рано равны, их суммарный лимсуп логарифма по n совпадает.

LaTeX

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

Lean4

theorem expGrowthSup_congr (h : u =ᶠ[atTop] v) : expGrowthSup u = expGrowthSup v :=
  limsup_congr (h.mono fun _ uv ↦ uv ▸ rfl)

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