of_isEquivalent_const

Mathlib.Computability.AkraBazzi.GrowsPolynomially

URI: https://scilib.ai/kg/mathlib#AkraBazziRecurrence.GrowsPolynomially.of_isEquivalent_const

English

If f is asymptotically equivalent to a constant function, then f grows polynomially.

Русский

Если f асимптотически эквивалентна константе, то f растёт полиномиально.

LaTeX

$$$f \\sim_{atTop} c \\Rightarrow \\text{GrowsPolynomially}(f)$$$

Lean4

theorem of_isEquivalent_const {f : ℝ → ℝ} {c : ℝ} (hf : f ~[atTop] fun _ => c) : GrowsPolynomially f :=
  of_isEquivalent growsPolynomially_const hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru