English
If the partial sums of a function f grow at most like n^r (Big-O), then the associated L-series converges at every s with Re(s) > r.
Русский
Если сумма по модулю частичных сумм f(k) растёт не быстрее чем n^r (Big-O), то соответствующая L-функция сходится при Re(s) > r.
LaTeX
$$$LSeriesSummable(f, s) \\quad \\text{provided} \\quad (\\sum_{k=1}^{n} \\|f(k)\\|) = O(n^{r}) \\text{ and } r < \\Re(s)$$$
Lean4
/-- If 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 (hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ (n : ℝ) ^ r)
(hr : 0 ≤ r) (hs : r < s.re) : LSeriesSummable f s :=
by
have h₁ : (fun n ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f := by
filter_upwards [eventually_ne_atTop 0] with n hn using by simp_rw [if_neg hn]
refine (LSeriesSummable_of_sum_norm_bigO_aux (if_pos rfl) ?_ hr hs).congr' _ h₁
refine hO.congr' (Eventually.of_forall fun _ ↦ Finset.sum_congr rfl fun _ h ↦ ?_) EventuallyEq.rfl
rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']
