English
If f has controlled growth (Big-O) and L-series converges for Re(s) > r, then LSeries f(s) equals s times the integral over t>1 of the partial sums up to ⌊t⌋ times t^{-(s+1)}.
Русский
ЕслиL-функция имеет управляемый рост и сходится при Re(s) > r, то LSeries f(s) = s ∫_{1}^{∞} (частичные суммы) t^{-(s+1)} dt.
LaTeX
$$$LSeries(f,s) = s \\int_{1}^{\infty} (\\sum_{k ≤ ⌊t⌋} f(k)) t^{-(s+1)} dt$$$
Lean4
/-- If the partial sums `∑ k ∈ Icc 1 n, f k` are `O(n ^ r)` for some real `0 ≤ r` and the
L-series `LSeries f` converges at `s : ℂ` with `r < s.re`, then
`LSeries f s = s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (-(s + 1))`. -/
theorem LSeries_eq_mul_integral (f : ℕ → ℂ) {r : ℝ} (hr : 0 ≤ r) {s : ℂ} (hs : r < s.re) (hS : LSeriesSummable f s)
(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)) :=
by
rw [←
LSeriesSummable_congr' s (f := fun n ↦ if n = 0 then 0 else f n)
(by filter_upwards [eventually_ne_atTop 0] with n h using if_neg h)] at hS
have (n : _) : ∑ k ∈ Icc 1 n, (if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k :=
Finset.sum_congr rfl fun k hk ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp hk).1).ne']
rw [← LSeries_congr fun _ ↦ if_neg _, LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS] <;> simp_all
