isBigO_rpow — Mathlib

English

If LSeriesSummable f s then f = O( n^{Re(s)} ) atTop.

Русский

Если L-серия суммируема, то f = O(n^{Re(s)}) на atTop.

LaTeX

$$LSeriesSummable(f,s) → f =O[atTop] (n^{s.re})$$

Lean4

/-- If the `LSeries` of `f` is summable at `s`, then `f = O(n^(re s))`. -/
theorem isBigO_rpow {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) : f =O[atTop] fun n ↦ (n : ℝ) ^ s.re :=
  by
  obtain ⟨C, hC⟩ := h.le_const_mul_rpow
  refine Asymptotics.IsBigO.of_bound C <| eventually_atTop.mpr ⟨1, fun n hn ↦ ?_⟩
  convert hC n (Nat.pos_iff_ne_zero.mp hn) using 2
  rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg n.cast_nonneg, abs_of_nonneg n.cast_nonneg]

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