LSeriesSummable_of_bounded_of_one_lt_re

English

If f = O(n^{x-1}) and Re(s) > x, then LSeriesSummable f s.

Русский

Если f = O(n^{x-1}) и Re(s) > x, тогда LSeriesSummable f s.

LaTeX

$$Real.instLT.lt x s.re ∧ (f =O[atTop] n^{x-1}) → LSeriesSummable f s$$

Lean4

/-- If `f` is bounded, then its `LSeries` is summable at `s` when `re s > 1`. -/
theorem LSeriesSummable_of_bounded_of_one_lt_re {f : ℕ → ℂ} {m : ℝ} (h : ∀ n ≠ 0, ‖f n‖ ≤ m) {s : ℂ} (hs : 1 < s.re) :
    LSeriesSummable f s :=
  LSeriesSummable_of_le_const_mul_rpow hs ⟨m, fun n hn ↦ by simp [h n hn]⟩

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