trans_le

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleO.trans_le

English

If f = o_l g and ∀ x, ||g(x)|| ≤ ||k(x)||, then f = o_l k with the appropriate c.

Русский

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

LaTeX

$$$f = o\; l\; g \land (\forall x, \|g(x)\| ≤ \|k(x)\|) \Rightarrow f = o\; l\; k$$$

Lean4

theorem trans_le (hfg : f =o[l] g) (hgk : ∀ x, ‖g x‖ ≤ ‖k x‖) : f =o[l] k :=
  hfg.trans_isBigOWith (isBigOWith_of_le _ hgk) zero_lt_one

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

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

Разделы

Аффилиация

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