right_isBigO_add — Mathlib

English

If f1 = o[l] f2, then there is a Big-O relation between f2 and f2−f1, and vice versa via a standard bound.

Русский

Если f1 = o[l] f2, то можно установить отношение Big-O между f2 и (f2−f1), и наоборот.

LaTeX

$$$\\displaystyle (f_1 = o_l f_2) \\Rightarrow (f_2 = O_l (f_2 - f_1))$, and conversely with a bounded constant.$$

Lean4

theorem right_isBigO_add {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] fun x => f₁ x + f₂ x :=
  ((h.def' one_half_pos).right_le_add_of_lt_one one_half_lt_one).isBigO

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