isBigO_top

Mathlib.Analysis.Asymptotics.Lemmas

URI: https://scilib.ai/kg/mathlib#Asymptotics.isBigO_top

English

Prime instance of isBigO_top with another copy; identical criterion for the top filter.

Русский

Повторение isBigO_top; одинаковое критерий для верхнего фильтра.

LaTeX

$$$f =O[top] g \iff \exists C, \forall x, \|f(x)\| ≤ C \|g(x)\|$$$

Lean4

@[simp]
theorem isBigO_top : f =O[⊤] g ↔ ∃ C, ∀ x, ‖f x‖ ≤ C * ‖g x‖ := by simp_rw [isBigO_iff, eventually_top]

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

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

Разделы

Аффилиация

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