tendsto_atTop_r

Mathlib.Computability.AkraBazzi.SumTransform

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

← MathLib Explorer

English

(1 − smoothingFn x) is asymptotically equivalent to 1 as x → ∞.

Русский

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

LaTeX

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

Lean4

theorem tendsto_atTop_r (i : α) : Tendsto (r i) atTop atTop :=
  by
  rw [tendsto_atTop]
  intro b
  have := R.eventually_r_ge b
  rw [Filter.eventually_all] at this
  exact_mod_cast this i

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

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

Разделы

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

Аффилиация

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