Even Hurwitz zeta functions

In this file we study the functions on ℂ which are the meromorphic continuation of the following series (convergent for 1 < re s), where a ∈ ℝ is a parameter:

completedHurwitzZetaEven a s = 1 / 2 * □ * ∑' n : ℤ, 1 / |n + a| ^ s

and

completedCosZeta a s = □ * ∑' n : ℕ, cos (2 * π * a * n) / |n| ^ s

where □ denotes a Gamma factor. Note that the term for n = -a in the first sum is omitted if a is an integer, and the term for n = 0 is omitted in the second sum (always).

Of course, we cannot define these functions by the above formulae (since existence of the meromorphic continuation is not at all obvious); we in fact construct them as Mellin transforms of various versions of the Jacobi theta function. We also define modified versions with a subscript 0 which are entire functions differing from the above by multiples of 1 / s and 1 / (1 - s).

## Main definitions and theorems

• completedHurwitzZetaEven: the completed Hurwitz zeta function
• completedCosZeta: the completed cosine zeta function
• differentiableAt_completedHurwitzZetaEven and differentiableAt_completedCosZeta: differentiability away from s = 0 and s = 1
• completedHurwitzZetaEven_one_sub: the functional equation completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
• completedHurwitzZetaEven_eq_tsum_int and completedCosZeta_eq_tsum_nat: relation between the zeta functions and corresponding Dirichlet series for 1 < re s

Definitions and elementary properties of kernels

@[irreducible]

def evenKernel (a : UnitAddCircle) (x : ℝ) : ℝ

Even Hurwitz zeta kernel (function whose Mellin transform will be the even part of the completed Hurwit zeta function). See evenKernel_def for the defining formula, and hasSum_int_evenKernel for an expression as a sum over ℤ.

Equations

• evenKernel a x = Function.Periodic.lift ⋯ a

theorem evenKernel_def (a : ℝ) (x : ℝ) : ↑(evenKernel (↑a) x) = Complex.exp (-↑Real.pi * ↑a ^ 2 * ↑x) * jacobiTheta₂ (↑a * Complex.I * ↑x) (Complex.I * ↑x)

theorem evenKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : evenKernel a x = 0

For x ≤ 0 the defining sum diverges, so the kernel is 0.

@[irreducible]

def cosKernel (a : UnitAddCircle) (x : ℝ) : ℝ

Cosine Hurwitz zeta kernel. See cosKernel_def for the defining formula, and hasSum_int_cosKernel for expression as a sum.

Equations

• cosKernel a x = Function.Periodic.lift ⋯ a

theorem cosKernel_def (a : ℝ) (x : ℝ) : ↑(cosKernel (↑a) x) = jacobiTheta₂ (↑a) (Complex.I * ↑x)

theorem cosKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : cosKernel a x = 0

theorem evenKernel_eq_cosKernel_of_zero : evenKernel 0 = cosKernel 0

For a = 0, both kernels agree.

theorem evenKernel_neg (a : UnitAddCircle) (x : ℝ) : evenKernel (-a) x = evenKernel a x

theorem cosKernel_neg (a : UnitAddCircle) (x : ℝ) : cosKernel (-a) x = cosKernel a x

theorem continuousOn_evenKernel (a : UnitAddCircle) : ContinuousOn (evenKernel a) (Set.Ioi 0)

theorem continuousOn_cosKernel (a : UnitAddCircle) : ContinuousOn (cosKernel a) (Set.Ioi 0)

theorem evenKernel_functional_equation (a : UnitAddCircle) (x : ℝ) : evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Formulae for the kernels as sums

theorem hasSum_int_evenKernel (a : ℝ) {t : ℝ} (ht : 0 < t) : HasSum (fun (n : ℤ) => Real.exp (-Real.pi * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t)

theorem hasSum_int_cosKernel (a : ℝ) {t : ℝ} (ht : 0 < t) : HasSum (fun (n : ℤ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) * ↑(Real.exp (-Real.pi * ↑n ^ 2 * t))) ↑(cosKernel (↑a) t)

theorem hasSum_int_evenKernel₀ (a : ℝ) {t : ℝ} (ht : 0 < t) : HasSum (fun (n : ℤ) => if ↑n + a = 0 then 0 else Real.exp (-Real.pi * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - if ↑a = 0 then 1 else 0)

Modified version of hasSum_int_evenKernel omitting the constant term at ∞.

theorem hasSum_int_cosKernel₀ (a : ℝ) {t : ℝ} (ht : 0 < t) : HasSum (fun (n : ℤ) => if n = 0 then 0 else Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) * ↑(Real.exp (-Real.pi * ↑n ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)

theorem hasSum_nat_cosKernel₀ (a : ℝ) {t : ℝ} (ht : 0 < t) : HasSum (fun (n : ℕ) => 2 * Real.cos (2 * Real.pi * a * (↑n + 1)) * Real.exp (-Real.pi * (↑n + 1) ^ 2 * t)) (cosKernel (↑a) t - 1)

Asymptotics of the kernels as t → ∞

theorem isBigO_atTop_evenKernel_sub (a : UnitAddCircle) : ∃ (p : ℝ), 0 < p ∧ (fun (x : ℝ) => evenKernel a x - if a = 0 then 1 else 0) =O[Filter.atTop] fun (x : ℝ) => Real.exp (-p * x)

The function evenKernel a - L has exponential decay at +∞, where L = 1 if a = 0 and L = 0 otherwise.

theorem isBigO_atTop_cosKernel_sub (a : UnitAddCircle) : ∃ (p : ℝ), 0 < p ∧ (fun (x : ℝ) => cosKernel a x - 1) =O[Filter.atTop] fun (x : ℝ) => Real.exp (-p * x)

The function cosKernel a - 1 has exponential decay at +∞, for any a.

Construction of a FE-pair

def hurwitzEvenFEPair (a : UnitAddCircle) : WeakFEPair ℂ

A WeakFEPair structure with f = evenKernel a and g = cosKernel a.

Equations

• One or more equations did not get rendered due to their size.

theorem hurwitzEvenFEPair_zero_symm : WeakFEPair.symm (hurwitzEvenFEPair 0) = hurwitzEvenFEPair 0

theorem hurwitzEvenFEPair_neg (a : UnitAddCircle) : hurwitzEvenFEPair (-a) = hurwitzEvenFEPair a

Definition of the completed even Hurwitz zeta function

def completedHurwitzZetaEven (a : UnitAddCircle) (s : ℂ) : ℂ

The meromorphic function of s which agrees with 1 / 2 * Gamma (s / 2) * π ^ (-s / 2) * ∑' (n : ℤ), 1 / |n + a| ^ s for 1 < re s.

Equations

• completedHurwitzZetaEven a s = WeakFEPair.Λ (hurwitzEvenFEPair a) (s / 2) / 2

def completedHurwitzZetaEven₀ (a : UnitAddCircle) (s : ℂ) : ℂ

The entire function differing from completedHurwitzZetaEven a s by a linear combination of 1 / s and 1 / (1 - s).

Equations

• completedHurwitzZetaEven₀ a s = WeakFEPair.Λ₀ (hurwitzEvenFEPair a) (s / 2) / 2

theorem completedHurwitzZetaEven_eq (a : UnitAddCircle) (s : ℂ) : completedHurwitzZetaEven a s = completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)

def completedCosZeta (a : UnitAddCircle) (s : ℂ) : ℂ

The meromorphic function of s which agrees with Gamma (s / 2) * π ^ (-s / 2) * ∑' n : ℕ, cos (2 * π * a * n) / n ^ s for 1 < re s.

Equations

• completedCosZeta a s = WeakFEPair.Λ (WeakFEPair.symm (hurwitzEvenFEPair a)) (s / 2) / 2

def completedCosZeta₀ (a : UnitAddCircle) (s : ℂ) : ℂ

The entire function differing from completedCosZeta a s by a linear combination of 1 / s and 1 / (1 - s).

Equations

• completedCosZeta₀ a s = WeakFEPair.Λ₀ (WeakFEPair.symm (hurwitzEvenFEPair a)) (s / 2) / 2

theorem completedCosZeta_eq (a : UnitAddCircle) (s : ℂ) : completedCosZeta a s = completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s)

Parity and functional equations

theorem completedHurwitzZetaEven_neg (a : UnitAddCircle) (s : ℂ) : completedHurwitzZetaEven (-a) s = completedHurwitzZetaEven a s

theorem completedHurwitzZetaEven₀_neg (a : UnitAddCircle) (s : ℂ) : completedHurwitzZetaEven₀ (-a) s = completedHurwitzZetaEven₀ a s

theorem completedCosZeta_neg (a : UnitAddCircle) (s : ℂ) : completedCosZeta (-a) s = completedCosZeta a s

theorem completedCosZeta₀_neg (a : UnitAddCircle) (s : ℂ) : completedCosZeta₀ (-a) s = completedCosZeta₀ a s

theorem completedHurwitzZetaEven_one_sub (a : UnitAddCircle) (s : ℂ) : completedHurwitzZetaEven a (1 - s) = completedCosZeta a s

Functional equation for the even Hurwitz zeta function.

theorem completedHurwitzZetaEven₀_one_sub (a : UnitAddCircle) (s : ℂ) : completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s

Functional equation for the even Hurwitz zeta function with poles removed.

theorem completedCosZeta_one_sub (a : UnitAddCircle) (s : ℂ) : completedCosZeta a (1 - s) = completedHurwitzZetaEven a s

Functional equation for the even Hurwitz zeta function (alternative form).

theorem completedCosZeta₀_one_sub (a : UnitAddCircle) (s : ℂ) : completedCosZeta₀ a (1 - s) = completedHurwitzZetaEven₀ a s

Functional equation for the even Hurwitz zeta function with poles removed (alternative form).