isLittleO_iff_nat_mul_le

Mathlib.Analysis.Asymptotics.Defs

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

← MathLib Explorer

English

If h is IsBigOWith c l f g and f1 ≡ f2 pointwise, then IsBigOWith c l f2 g.

Русский

Если h = IsBigOWith c l f g и f1(x) = f2(x) для всех x, то IsBigOWith c l f2 g.

LaTeX

$$$ IsBigOWith\ c\ l\ f\ g \rightarrow (f \equiv f' ) \Rightarrow IsBigOWith c l f' g $$$

Lean4

theorem isLittleO_iff_nat_mul_le : f =o[l] g' ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f x‖ ≤ ‖g' x‖ :=
  isLittleO_iff_nat_mul_le_aux (Or.inr fun _x => norm_nonneg _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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