English
If f takes nonnegative real values and its partial sums are O(n^r), then the integral formula for L-series holds with f(k) treated as complex numbers.
Русский
Если f(k) неотрицательно и частичные суммы равны O(n^r), то формула интеграла для L-функции сохраняется при интерпретации f(k) как комплексных чисел.
LaTeX
$$$LSeries( f ) (s) = s \\int_{1}^{\\infty} (\\sum_{k ≤ ⌊t⌋} (f(k) : \\mathbb{C})) t^{-(s+1)} dt$$$
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 for `s : ℂ` with `r < s.re`, we have
`LSeries f s = s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (-(s + 1))`. -/
theorem LSeries_eq_mul_integral_of_nonneg (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) (hf : ∀ n, 0 ≤ f n) :
LSeries (fun n ↦ f n) s = s * ∫ t in Set.Ioi (1 : ℝ), (∑ k ∈ Icc 1 ⌊t⌋₊, (f k : ℂ)) * t ^ (-(s + 1)) :=
LSeries_eq_mul_integral' _ hr hs <| hO.congr_left fun _ ↦ by simp [abs_of_nonneg (hf _)]
