isLittleO_abs_right

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.isLittleO_abs_right

English

The absolute-value bound is equivalent to the bound with the underlying real-valued function.

Русский

Граница по модулю эквивалентна границе по самой функции.

LaTeX

$$$IsBigOWith\ c\ l f (|u|) \iff IsBigOWith\ c\ l f u$$$

Lean4

@[simp]
theorem isLittleO_abs_right : (f =o[l] fun x => |u x|) ↔ f =o[l] u :=
  @isLittleO_norm_right _ _ ℝ _ _ _ _ _

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

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

Разделы

Аффилиация

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