isTheta

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

English

Asymptotic equivalence implies Theta-boundedness: u ~[l] v implies u =Θ[l] v.

Русский

Асимптотическая эквивалентность влечет за собой ограниченность по Theta: u ~[l] v.

LaTeX

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

Lean4

theorem isTheta (h : u ~[l] v) : u =Θ[l] v :=
  ⟨h.isBigO, h.isBigO_symm⟩

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

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

Разделы

Аффилиация

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