Theorems · Theorem · number theory

LSeries_eq_mul_integral

∀ (f : ℕ → ℂ) {r : ℝ},
  0 ≤ r →
    ∀ {s : ℂ},
      r < s.re →
        LSeriesSummable f s →
          ((fun n => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun n => ↑n ^ r) →
            LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Finset.Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

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)).

Defined in

Mathlib.NumberTheory.LSeries.SumCoeff

Cited by

1 results in Mathlib

Foundations

Depth 276 from the axioms · uses propext, Classical.choice, Quot.sound