isBigO

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyEq.isBigO

English

If f = O_l f' and ∀ x, ||f'(x)|| ≤ ||k(x)||, then f = O_l k.

Русский

Если f = O_l f' и ∀ x, ||f'(x)|| ≤ ||k(x)||, тогда f = O_l k.

LaTeX

$$$f = O_l f' \land (\forall x, \|f'(x)\| \le \|k(x)\|) \Rightarrow f = O_l k$$$

Lean4

theorem _root_.Filter.EventuallyEq.isBigO {f₁ f₂ : α → E} (hf : f₁ =ᶠ[l] f₂) : f₁ =O[l] f₂ :=
  hf.trans_isBigO (isBigO_refl _ _)

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

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

Разделы

Аффилиация

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