growsPolynomially_zpow

Mathlib.Computability.AkraBazzi.GrowsPolynomially

URI: https://scilib.ai/kg/mathlib#AkraBazziRecurrence.growsPolynomially_zpow

English

For any integer p, x^p grows polynomially.

Русский

Для любого целого p функция x^p растёт полиномиально.

LaTeX

$$$\\forall p \\in \\mathbb{Z},\\; \\text{GrowsPolynomially}(x \\mapsto x^{p})$$$

Lean4

theorem growsPolynomially_zpow (p : ℤ) : GrowsPolynomially fun x => x ^ p :=
  (growsPolynomially_id).zpow p (eventually_ge_atTop 0)

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

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

Разделы

Аффилиация

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