of_pow — Mathlib

English

For f: α → 𝕜, g: α → R, n ∈ ℕ, if n ≠ 0 and f^n =O_l (g^n), then f =O_l g.

Русский

Для f: α → 𝕜, g: α → R, n ≠ 0: если f^n = O_l g^n, то f = O_l g.

LaTeX

$$$ (f^n) =O[l] (g^n) \Rightarrow f =O[l] g \ (n \neq 0). $$$

Lean4

theorem of_pow {f : α → 𝕜} {g : α → R} {n : ℕ} (hn : n ≠ 0) (h : (f ^ n) =O[l] (g ^ n)) : f =O[l] g :=
  by
  rcases h.exists_pos with ⟨C, _hC₀, hC⟩
  obtain ⟨c : ℝ, hc₀ : 0 ≤ c, hc : C ≤ c ^ n⟩ :=
    ((eventually_ge_atTop _).and <| (tendsto_pow_atTop hn).eventually_ge_atTop C).exists
  exact (hC.of_pow hn hc hc₀).isBigO

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