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.

Equations

• HurwitzZeta.hurwitzZeta a s = HurwitzZeta.hurwitzZetaEven a s + HurwitzZeta.hurwitzZetaOdd a s

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

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

theorem HurwitzZeta.differentiableAt_hurwitzZeta (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 1) : DifferentiableAt ℂ (HurwitzZeta.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.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.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.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.hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) (nhds 1) (nhds (HurwitzZeta.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 : UnitAddCircle) (b : UnitAddCircle) : Differentiable ℂ fun (s : ℂ) => HurwitzZeta.hurwitzZeta a s - HurwitzZeta.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.

Equations

• HurwitzZeta.expZeta a s = HurwitzZeta.cosZeta a s + Complex.I * HurwitzZeta.sinZeta a s

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

theorem HurwitzZeta.sinZeta_eq (a : UnitAddCircle) (s : ℂ) : HurwitzZeta.sinZeta a s = (HurwitzZeta.expZeta a s - HurwitzZeta.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) (HurwitzZeta.expZeta (↑a) s)

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

theorem HurwitzZeta.differentiable_expZeta_of_ne_zero {a : UnitAddCircle} (ha : a ≠ 0) : Differentiable ℂ (HurwitzZeta.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 (HurwitzZeta.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.hurwitzZeta a (1 - s) = (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * (Complex.exp (-↑Real.pi * Complex.I * s / 2) * HurwitzZeta.expZeta a s + Complex.exp (↑Real.pi * Complex.I * s / 2) * HurwitzZeta.expZeta (-a) s)

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

Functional equation for the exponential zeta function.