The Hurwitz zeta function

This file gives the definition and properties of the following two functions:

• The Hurwitz zeta function, which is the meromorphic continuation to all s ∈ ℂ of the function defined for 1 < re s by the series

  ∑' n, 1 / (n + a) ^ s

  for a parameter a ∈ ℝ, with the sum taken over all n such that n + a > 0;

• the related sum, which we call the "exponential zeta function" (does it have a standard name?)

  ∑' n : ℕ, exp (2 * π * I * n * a) / n ^ s.

Main definitions and results

• hurwitzZeta: the Hurwitz zeta function (defined to be periodic in a with period 1)
• expZeta: the exponential zeta function
• hasSum_hurwitzZeta_of_one_lt_re and hasSum_expZeta_of_one_lt_re: relation to Dirichlet series for 1 < re s
• hurwitzZeta_residue_one shows that the residue at s = 1 equals 1
• differentiableAt_hurwitzZeta and differentiableAt_expZeta: analyticity away from s = 1
• hurwitzZeta_one_sub and expZeta_one_sub: functional equations s ↔ 1 - s.

The Hurwitz zeta function

noncomputable def HurwitzZeta.hurwitzZeta (a : UnitAddCircle) (s : ℂ) : ℂ

The Hurwitz zeta function, which is the meromorphic continuation of ∑ (n : ℕ), 1 / (n + a) ^ s if 0 ≤ a ≤ 1. See hasSum_hurwitzZeta_of_one_lt_re for the relation to the Dirichlet series in the convergence range.

theorem HurwitzZeta.hurwitzZetaEven_eq (a : UnitAddCircle) (s : ℂ) : hurwitzZetaEven a s = (hurwitzZeta a s + hurwitzZeta (-a) s) / 2

theorem HurwitzZeta.hurwitzZetaOdd_eq (a : UnitAddCircle) (s : ℂ) : hurwitzZetaOdd a s = (hurwitzZeta a s - hurwitzZeta (-a) s) / 2

theorem HurwitzZeta.differentiableAt_hurwitzZeta (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 1) : DifferentiableAt ℂ (hurwitzZeta a) s

The Hurwitz zeta function is differentiable away from s = 1.

theorem HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re {a : ℝ} (ha : a ∈ Set.Icc 0 1) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (n : ℕ) => 1 / (↑n + ↑a) ^ s) (hurwitzZeta (↑a) s)

Formula for hurwitzZeta s as a Dirichlet series in the convergence range. We restrict to a ∈ Icc 0 1 to simplify the statement.

theorem HurwitzZeta.hurwitzZeta_residue_one (a : UnitAddCircle) : Filter.Tendsto (fun (s : ℂ) => (s - 1) * hurwitzZeta a s) (nhdsWithin 1 {1}ᶜ) (nhds 1)

The residue of the Hurwitz zeta function at s = 1 is 1.

theorem HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div (a : UnitAddCircle) : DifferentiableAt ℂ (fun (s : ℂ) => hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) 1

theorem HurwitzZeta.tendsto_hurwitzZeta_sub_one_div_nhds_one (a : UnitAddCircle) : Filter.Tendsto (fun (s : ℂ) => hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) (nhds 1) (nhds (hurwitzZeta a 1))

Expression for hurwitzZeta a 1 as a limit. (Mathematically hurwitzZeta a 1 is undefined, but our construction assigns some value to it; this lemma is mostly of interest for determining what that value is).

theorem HurwitzZeta.differentiable_hurwitzZeta_sub_hurwitzZeta (a b : UnitAddCircle) : Differentiable ℂ fun (s : ℂ) => hurwitzZeta a s - hurwitzZeta b s

The difference of two Hurwitz zeta functions is differentiable everywhere.

The exponential zeta function

noncomputable def HurwitzZeta.expZeta (a : UnitAddCircle) (s : ℂ) : ℂ

Meromorphic continuation of the series ∑' (n : ℕ), exp (2 * π * I * a * n) / n ^ s. See hasSum_expZeta_of_one_lt_re for the relation to the Dirichlet series.

theorem HurwitzZeta.cosZeta_eq (a : UnitAddCircle) (s : ℂ) : cosZeta a s = (expZeta a s + expZeta (-a) s) / 2

theorem HurwitzZeta.sinZeta_eq (a : UnitAddCircle) (s : ℂ) : sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * Complex.I)

theorem HurwitzZeta.hasSum_expZeta_of_one_lt_re (a : ℝ) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (n : ℕ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) / ↑n ^ s) (expZeta (↑a) s)

theorem HurwitzZeta.differentiableAt_expZeta (a : UnitAddCircle) (s : ℂ) (hs : s ≠ 1 ∨ a ≠ 0) : DifferentiableAt ℂ (expZeta a) s

theorem HurwitzZeta.differentiable_expZeta_of_ne_zero {a : UnitAddCircle} (ha : a ≠ 0) : Differentiable ℂ (expZeta a)

If a ≠ 0 then the exponential zeta function is analytic everywhere.

theorem HurwitzZeta.LSeriesHasSum_exp (a : ℝ) {s : ℂ} (hs : 1 < s.re) : LSeriesHasSum (fun (x : ℕ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑x)) s (expZeta (↑a) s)

Reformulation of hasSum_expZeta_of_one_lt_re using LSeriesHasSum.

The functional equation

theorem HurwitzZeta.hurwitzZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) (hs' : a ≠ 0 ∨ s ≠ 1) : hurwitzZeta a (1 - s) = (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * (Complex.exp (-↑Real.pi * Complex.I * s / 2) * expZeta a s + Complex.exp (↑Real.pi * Complex.I * s / 2) * expZeta (-a) s)

theorem HurwitzZeta.expZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ 1 - ↑n) : expZeta a (1 - s) = (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * (Complex.exp (↑Real.pi * Complex.I * s / 2) * hurwitzZeta a s + Complex.exp (-↑Real.pi * Complex.I * s / 2) * hurwitzZeta (-a) s)

Functional equation for the exponential zeta function.