Theorems · Theorem · number theory

HurwitzZeta.hasSum_int_completedSinZeta

∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum
      (fun n => (s + 1).Gammaℝ * -Complex.I * ↑n.sign * Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2)
      (HurwitzZeta.completedSinZeta (↑a) s)

Formula for completedSinZeta as a Dirichlet series in the convergence range (first version, with sum over ℤ).

Defined in

Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Cited by

2 results in Mathlib

Foundations

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