comp_neg_int

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigO.comp_neg_int

← MathLib Explorer

English

If f = O[map k l] g, then equivalently (f ∘ k) = O[l] (g ∘ k).

Русский

Если f = O[map k l] g, то эквивалентно (f ∘ k) = O[l] (g ∘ k).

LaTeX

$$$ f = O[map\ k\ l]\, g \iff (f\circ k) = O[l] (g\circ k) $$$

Lean4

theorem comp_neg_int {f : ℤ → E} {g : ℤ → F} (hf : f =O[cofinite] g) : (fun n => f (-n)) =O[cofinite] fun n => g (-n) :=
  by
  rw [← Equiv.neg_apply]
  exact hf.comp_tendsto (Equiv.neg ℤ).injective.tendsto_cofinite

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

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

Разделы

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

Аффилиация

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