isBigO_completion_right

Mathlib.Analysis.Asymptotics.Completion

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

English

The right-hand Big-O relation is preserved when passing to the completion space.

Русский

Относительно правого Big-O сохранение при переходе в пространство дополнения сохраняется.

LaTeX

$$$ IsBigO(l, f, g) \iff IsBigO(l, f, (\hat{g})) $$$

Lean4

@[simp, norm_cast]
theorem isBigO_completion_right : f =O[l] (fun x ↦ g x : α → F̂) ↔ f =O[l] g := by simp only [isBigO_iff, norm_coe]

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

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

Разделы

Аффилиация

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