rpow

Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

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

← MathLib Explorer

English

If f = Θ_l g, then f^r = Θ_l g^r for r ≥ 0.

Русский

Если f = Θ_l g, то f^r = Θ_l g^r при r ≥ 0.

LaTeX

$$$$ f^r = Θ_l \ g^r \quad (r \ge 0). $$$$

Lean4

theorem rpow (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) (h : f =O[l] g) : (fun x => f x ^ r) =O[l] fun x => g x ^ r :=
  let ⟨_, hc, h'⟩ := h.exists_nonneg
  (h'.rpow hc hr hg).isBigO

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

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

Разделы

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

Аффилиация

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