isBigO_symm

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsEquivalent.isBigO_symm

English

If u ~[l] v, then v =O[l] u (and equivalently u =O[l] v by symmetry).

Русский

Если u эквивалентна v вдоль l, то v растёт не быстрее u (Big-O), и наоборот по симметрии.

LaTeX

$$$u ~[l] v \Rightarrow v =O[l] u$$$

Lean4

theorem isBigO_symm (h : u ~[l] v) : v =O[l] u :=
  by
  convert h.isLittleO.right_isBigO_add
  simp

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

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

Разделы

Аффилиация

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