Theorems · Theorem · number theory

HurwitzZeta.hasSum_int_completedCosZeta

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

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

Defined in

Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Cited by

2 results in Mathlib

Foundations

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