isEquivalent_one_sub_smoothingFn_one

Mathlib.Computability.AkraBazzi.SumTransform

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

← MathLib Explorer

English

(1 − smoothingFn x) is asymptotically equivalent to 1.

Русский

(1 − сглаживающая функция x) асимптотически эквивалентна 1.

LaTeX

$$$ (1 - \varepsilon x) \sim_{atTop} 1 $$$

Lean4

theorem isEquivalent_one_sub_smoothingFn_one : (fun x => 1 - ε x) ~[atTop] (fun _ => (1 : ℝ)) :=
  IsEquivalent.sub_isLittleO IsEquivalent.refl isLittleO_smoothingFn_one

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

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

Разделы

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

Аффилиация

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