English
If f: ℕ → ℝ with nonnegativity and a Big-O bound holds, then the limit of (s−1) LSeries(f)(s) as s → 1^+ equals the same limit as the average of partial sums, along the positive real axis.
Русский
Если f: ℕ → ℝ неотрицательна и выполняется ограничение Big-O, то предел (s−1) LSeries(f)(s) при s → 1^+ совпадает с пределом среднего значения частичных сумм.
LaTeX
$$$\\lim_{s \\to 1^+} (s-1) LSeries(f,s) = l$ where $l = \\lim_{n\\to\\infty} \\frac{1}{n} \\sum_{k=1}^n f(k)$ and $f: \\mathbb{N} \\to \\mathbb{R}_{\\ge 0}$ with appropriate summability.$$
Lean4
theorem LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg (f : ℕ → ℝ) {l : ℝ}
(hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / (n : ℝ)) atTop (𝓝 l)) (hf' : ∀ n, 0 ≤ f n) :
Tendsto (fun s : ℝ ↦ (s - 1) * LSeries (fun n ↦ f n) s) (𝓝[>] 1) (𝓝 l) :=
by
refine
LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div (f := fun n ↦ f n) (hf.ofReal.congr fun _ ↦ ?_) fun s hs ↦ ?_
· simp
· refine LSeriesSummable_of_sum_norm_bigO_and_nonneg ?_ hf' zero_le_one hs
exact isBigO_atTop_natCast_rpow_of_tendsto_div_rpow (by simpa)
