English
A variant of the integral representation requiring only the stronger Big-O bound on partial sums; the L-series equals s times the corresponding integral.
Русский
Вариант интегрального представления требует только более сильного условия Big-O для частичных сумм; LSeries равно sжды соответствующему интегралу.
LaTeX
$$$LSeries(f,s) = s \\int_{1}^{\\infty} (\\sum_{k ≤ ⌊t⌋} f(k)) t^{-(s+1)} dt$ under strengthened Big-O$$
Lean4
/-- A version of `LSeries_eq_mul_integral` where we use the stronger condition that the partial sums
`∑ k ∈ Icc 1 n, ‖f k‖` are `O(n ^ r)` to deduce the integral representation. -/
theorem LSeries_eq_mul_integral' (f : ℕ → ℂ) {r : ℝ} (hr : 0 ≤ r) {s : ℂ} (hs : r < s.re)
(hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ (n : ℝ) ^ r) :
LSeries f s = s * ∫ t in Set.Ioi (1 : ℝ), (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (-(s + 1)) :=
LSeries_eq_mul_integral _ hr hs (LSeriesSummable_of_sum_norm_bigO hO hr hs) <|
(isBigO_of_le _ fun _ ↦ (norm_sum_le _ _).trans <| Real.le_norm_self _).trans hO
