growsPolynomially_one_sub_smoothingFn

Mathlib.Computability.AkraBazzi.SumTransform

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

← MathLib Explorer

English

The function x ↦ 1 − smoothingFn x grows polynomially.

Русский

Функция x ↦ 1 − сглаживающая функция растет полиномиально.

LaTeX

$$GrowsPolynomially (fun x => 1 - (smoothingFn x))$$

Lean4

theorem growsPolynomially_one_sub_smoothingFn : GrowsPolynomially fun x => 1 - ε x :=
  GrowsPolynomially.of_isEquivalent_const isEquivalent_one_sub_smoothingFn_one

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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