of_bound'

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigO.of_bound'

English

If eventually the norm of f is bounded above by the real-valued function g, then f =O[l] g.

Русский

Если существует событие, что норма f ниже g, то f =O[l] g.

LaTeX

$$IsBigO.of_norm_eventuallyLE {g : α → ℝ} (h : (‖f‖) ≤^ᶠ[l] g) : f =O[l] g$$

Lean4

theorem of_bound' (h : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖) : f =O[l] g :=
  .of_bound 1 <| by simpa only [one_mul] using h

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

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

Разделы

Аффилиация

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