pow — Mathlib

English

If f^n = O_l(g^n) with n ≠ 0, and constants satisfy c ≤ c'^n and c' ≥ 0, then f = O_l(g) with bound c'.

Русский

Если f^n = O_l(g^n) при n ≠ 0 и существуют константы c ≤ c'^n и c' ≥ 0, то f = O_l(g) с константой c'.

LaTeX

$$$(f^n) =O_l(g^n) \\land n \\neq 0 \\land c \\le c'^n \\land c' \\ge 0 \\Rightarrow f =O_l(g) \\text{ with bound } c'.$$$

Lean4

theorem pow [NormOneClass S] {f : α → R} {g : α → S} (h : f =O[l] g) (n : ℕ) :
    (fun x => f x ^ n) =O[l] fun x => g x ^ n :=
  let ⟨_C, hC⟩ := h.isBigOWith
  isBigO_iff_isBigOWith.2 ⟨_, hC.pow' n⟩

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