isTheta_congr_left

Mathlib.Analysis.Asymptotics.Theta

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsTheta.isTheta_congr_left

English

If the norm of f' is Θ_l g', then f' and g' have the same Theta relation.

Русский

Если нормa f' эквивалентна g' по Θ_l, то f' и g' имеют общую Theta-отношение.

LaTeX

$$$\\|f'\\| =Θ_l g' \\Rightarrow f' =Θ_l g'$$$

Lean4

theorem isTheta_congr_left (h : f' =Θ[l] g') : f' =Θ[l] k ↔ g' =Θ[l] k :=
  h.isBigO_congr_left.and h.isBigO_congr_right

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

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

Разделы

Аффилиация

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