isBigO_atTop_natCast_rpow_of_tendsto_div_rpow

English

If g: ℕ → 𝕜 satisfies Tendsto (g(n)/n^r) to a, then g = O_atTop n^r.

Русский

Если g: ℕ → 𝕜 удовлетворяет пределу g(n)/n^r → a, то g = O_atTop n^r.

LaTeX

$$$$ g = O_{\mathrm{atTop}} \bigl(n \mapsto n^r\bigr) $$$$

Lean4

theorem isBigO_atTop_natCast_rpow_of_tendsto_div_rpow {𝕜 : Type*} [RCLike 𝕜] {g : ℕ → 𝕜} {a : 𝕜} {r : ℝ}
    (hlim : Tendsto (fun n ↦ g n / (n ^ r : ℝ)) atTop (𝓝 a)) : g =O[atTop] fun n ↦ (n : ℝ) ^ r :=
  by
  refine (isBigO_of_div_tendsto_nhds ?_ ‖a‖ ?_).of_norm_left
  · filter_upwards [eventually_ne_atTop 0] with _ h
    simp [Real.rpow_eq_zero_iff_of_nonneg, h]
  · exact hlim.norm.congr fun n ↦ by simp [abs_of_nonneg, show 0 ≤ (n : ℝ) ^ r by positivity]

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