LSeriesSummable_of_sum_norm_bigO_and_nonneg

English

If a nonnegative f has partial sums O(n^r) and r ≥ 0, then LSeries converges for s with Re(s) > r.

Русский

Если f(k) ≥ 0 и частичные суммы имеют порядок O(n^r) с r ≥ 0, то L-ряд сходится для Re(s) > r.

LaTeX

$$$LSeriesSummable(f, s) \\quad \\text{for } f: \\mathbb{N} \\to \\mathbb{R}, \\ r \\ge 0, \\ Re(s) > r$$$

Lean4

/-- If `f` takes nonnegative real values and the partial sums `∑ k ∈ Icc 1 n, f k` are `O(n ^ r)`
for some real `0 ≤ r`, then the L-series `LSeries f` converges at `s : ℂ` for all `s`
such that `r < s.re`. -/
theorem LSeriesSummable_of_sum_norm_bigO_and_nonneg {f : ℕ → ℝ}
    (hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ (n : ℝ) ^ r) (hf : ∀ n, 0 ≤ f n) (hr : 0 ≤ r) (hs : r < s.re) :
    LSeriesSummable (fun n ↦ f n) s :=
  LSeriesSummable_of_sum_norm_bigO (by simpa [abs_of_nonneg (hf _)]) hr hs

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