Odd Hurwitz zeta functions

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

hurwitzZetaOdd a s = 1 / 2 * ∑' n : ℤ, sgn (n + a) / |n + a| ^ s

and

sinZeta a s = ∑' n : ℕ, sin (2 * π * a * n) / n ^ s.

The term for n = -a in the first sum is understood as 0 if a is an integer, as is the term for n = 0 in the second sum (for all a). Note that these functions are differentiable everywhere, unlike their even counterparts which have poles.

Of course, we cannot define these functions by the above formulae (since existence of the analytic continuation is not at all obvious); we in fact construct them as Mellin transforms of various versions of the Jacobi theta function.

Main definitions and theorems

• completedHurwitzZetaOdd: the completed Hurwitz zeta function
• completedSinZeta: the completed cosine zeta function
• differentiable_completedHurwitzZetaOdd and differentiable_completedSinZeta: differentiability on ℂ
• completedHurwitzZetaOdd_one_sub: the functional equation completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s
• hasSum_int_hurwitzZetaOdd and hasSum_nat_sinZeta: relation between the zeta functions and corresponding Dirichlet series for 1 < re s

Definitions and elementary properties of kernels

def HurwitzZeta.jacobiTheta₂'' (z τ : ℂ) : ℂ

Variant of jacobiTheta₂' which we introduce to simplify some formulae.

Equations

• HurwitzZeta.jacobiTheta₂'' z τ = Complex.exp (↑Real.pi * Complex.I * z ^ 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * ↑Real.pi * Complex.I) + z * jacobiTheta₂ (z * τ) τ)

theorem HurwitzZeta.jacobiTheta₂''_conj (z τ : ℂ) : (starRingEnd ℂ) (HurwitzZeta.jacobiTheta₂'' z τ) = HurwitzZeta.jacobiTheta₂'' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

theorem HurwitzZeta.jacobiTheta₂''_add_left (z τ : ℂ) : HurwitzZeta.jacobiTheta₂'' (z + 1) τ = HurwitzZeta.jacobiTheta₂'' z τ

Restatement of jacobiTheta₂'_add_left': the function jacobiTheta₂'' is 1-periodic in z.

theorem HurwitzZeta.jacobiTheta₂''_neg_left (z τ : ℂ) : HurwitzZeta.jacobiTheta₂'' (-z) τ = -HurwitzZeta.jacobiTheta₂'' z τ

theorem HurwitzZeta.jacobiTheta₂'_functional_equation' (z τ : ℂ) : jacobiTheta₂' z τ = -2 * ↑Real.pi / (-Complex.I * τ) ^ (3 / 2) * HurwitzZeta.jacobiTheta₂'' z (-1 / τ)

@[irreducible]

def HurwitzZeta.oddKernel (a : UnitAddCircle) (x : ℝ) : ℝ

Odd Hurwitz zeta kernel (function whose Mellin transform will be the odd part of the completed Hurwitz zeta function). See oddKernel_def for the defining formula, and hasSum_int_oddKernel for an expression as a sum over ℤ.

Equations

• HurwitzZeta.oddKernel a x = ⋯.lift a

theorem HurwitzZeta.oddKernel_def (a x : ℝ) : ↑(HurwitzZeta.oddKernel (↑a) x) = HurwitzZeta.jacobiTheta₂'' (↑a) (Complex.I * ↑x)

theorem HurwitzZeta.oddKernel_def' (a x : ℝ) : ↑(HurwitzZeta.oddKernel (↑a) x) = Complex.exp (-↑Real.pi * ↑a ^ 2 * ↑x) * (jacobiTheta₂' (↑a * Complex.I * ↑x) (Complex.I * ↑x) / (2 * ↑Real.pi * Complex.I) + ↑a * jacobiTheta₂ (↑a * Complex.I * ↑x) (Complex.I * ↑x))

theorem HurwitzZeta.oddKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : HurwitzZeta.oddKernel a x = 0

@[irreducible]

def HurwitzZeta.sinKernel (a : UnitAddCircle) (x : ℝ) : ℝ

Auxiliary function appearing in the functional equation for the odd Hurwitz zeta kernel, equal to ∑ (n : ℕ), 2 * n * sin (2 * π * n * a) * exp (-π * n ^ 2 * x). See hasSum_nat_sinKernel for the defining sum.

Equations

• HurwitzZeta.sinKernel a x = ⋯.lift a

theorem HurwitzZeta.sinKernel_def (a x : ℝ) : ↑(HurwitzZeta.sinKernel (↑a) x) = jacobiTheta₂' (↑a) (Complex.I * ↑x) / (-2 * ↑Real.pi)

theorem HurwitzZeta.sinKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : HurwitzZeta.sinKernel a x = 0

theorem HurwitzZeta.oddKernel_neg (a : UnitAddCircle) (x : ℝ) : HurwitzZeta.oddKernel (-a) x = -HurwitzZeta.oddKernel a x

theorem HurwitzZeta.oddKernel_zero (x : ℝ) : HurwitzZeta.oddKernel 0 x = 0

theorem HurwitzZeta.sinKernel_neg (a : UnitAddCircle) (x : ℝ) : HurwitzZeta.sinKernel (-a) x = -HurwitzZeta.sinKernel a x

theorem HurwitzZeta.sinKernel_zero (x : ℝ) : HurwitzZeta.sinKernel 0 x = 0

theorem HurwitzZeta.continuousOn_oddKernel (a : UnitAddCircle) : ContinuousOn (HurwitzZeta.oddKernel a) (Set.Ioi 0)

The odd kernel is continuous on Ioi 0.

theorem HurwitzZeta.continuousOn_sinKernel (a : UnitAddCircle) : ContinuousOn (HurwitzZeta.sinKernel a) (Set.Ioi 0)

theorem HurwitzZeta.oddKernel_functional_equation (a : UnitAddCircle) (x : ℝ) : HurwitzZeta.oddKernel a x = 1 / x ^ (3 / 2) * HurwitzZeta.sinKernel a (1 / x)

Formulae for the kernels as sums

theorem HurwitzZeta.hasSum_int_oddKernel (a : ℝ) {x : ℝ} (hx : 0 < x) : HasSum (fun (n : ℤ) => (↑n + a) * Real.exp (-Real.pi * (↑n + a) ^ 2 * x)) (HurwitzZeta.oddKernel (↑a) x)

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

theorem HurwitzZeta.hasSum_nat_sinKernel (a : ℝ) {t : ℝ} (ht : 0 < t) : HasSum (fun (n : ℕ) => 2 * ↑n * Real.sin (2 * Real.pi * a * ↑n) * Real.exp (-Real.pi * ↑n ^ 2 * t)) (HurwitzZeta.sinKernel (↑a) t)

Asymptotics of the kernels as t → ∞

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

The function oddKernel a has exponential decay at +∞, for any a.

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

The function sinKernel a has exponential decay at +∞, for any a.

Construction of an FE-pair

def HurwitzZeta.hurwitzOddFEPair (a : UnitAddCircle) : StrongFEPair ℂ

A StrongFEPair structure with f = oddKernel a and g = sinKernel a.

Equations

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

@[simp]

theorem HurwitzZeta.hurwitzOddFEPair_ε (a : UnitAddCircle) : (HurwitzZeta.hurwitzOddFEPair a).ε = 1

@[simp]

theorem HurwitzZeta.hurwitzOddFEPair_g (a : UnitAddCircle) (a✝ : ℝ) : (HurwitzZeta.hurwitzOddFEPair a).g a✝ = (Complex.ofReal ∘ HurwitzZeta.sinKernel a) a✝

@[simp]

theorem HurwitzZeta.hurwitzOddFEPair_g₀ (a : UnitAddCircle) : (HurwitzZeta.hurwitzOddFEPair a).g₀ = 0

@[simp]

theorem HurwitzZeta.hurwitzOddFEPair_k (a : UnitAddCircle) : (HurwitzZeta.hurwitzOddFEPair a).k = 3 / 2

@[simp]

theorem HurwitzZeta.hurwitzOddFEPair_f (a : UnitAddCircle) (a✝ : ℝ) : (HurwitzZeta.hurwitzOddFEPair a).f a✝ = (Complex.ofReal ∘ HurwitzZeta.oddKernel a) a✝

@[simp]

theorem HurwitzZeta.hurwitzOddFEPair_f₀ (a : UnitAddCircle) : (HurwitzZeta.hurwitzOddFEPair a).f₀ = 0

Definition of the completed odd Hurwitz zeta function

def HurwitzZeta.completedHurwitzZetaOdd (a : UnitAddCircle) (s : ℂ) : ℂ

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

Equations

• HurwitzZeta.completedHurwitzZetaOdd a s = (HurwitzZeta.hurwitzOddFEPair a).Λ ((s + 1) / 2) / 2

theorem HurwitzZeta.differentiable_completedHurwitzZetaOdd (a : UnitAddCircle) : Differentiable ℂ (HurwitzZeta.completedHurwitzZetaOdd a)

def HurwitzZeta.completedSinZeta (a : UnitAddCircle) (s : ℂ) : ℂ

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

Equations

• HurwitzZeta.completedSinZeta a s = (HurwitzZeta.hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2

theorem HurwitzZeta.differentiable_completedSinZeta (a : UnitAddCircle) : Differentiable ℂ (HurwitzZeta.completedSinZeta a)

Parity and functional equations

theorem HurwitzZeta.completedHurwitzZetaOdd_neg (a : UnitAddCircle) (s : ℂ) : HurwitzZeta.completedHurwitzZetaOdd (-a) s = -HurwitzZeta.completedHurwitzZetaOdd a s

theorem HurwitzZeta.completedSinZeta_neg (a : UnitAddCircle) (s : ℂ) : HurwitzZeta.completedSinZeta (-a) s = -HurwitzZeta.completedSinZeta a s

theorem HurwitzZeta.completedHurwitzZetaOdd_one_sub (a : UnitAddCircle) (s : ℂ) : HurwitzZeta.completedHurwitzZetaOdd a (1 - s) = HurwitzZeta.completedSinZeta a s

Functional equation for the odd Hurwitz zeta function.

theorem HurwitzZeta.completedSinZeta_one_sub (a : UnitAddCircle) (s : ℂ) : HurwitzZeta.completedSinZeta a (1 - s) = HurwitzZeta.completedHurwitzZetaOdd a s

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

Relation to the Dirichlet series for 1 < re s

theorem HurwitzZeta.hasSum_int_completedSinZeta (a : ℝ) {s : ℂ} (hs : 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 ℤ).

theorem HurwitzZeta.hasSum_nat_completedSinZeta (a : ℝ) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (n : ℕ) => (s + 1).Gammaℝ * ↑(Real.sin (2 * Real.pi * a * ↑n)) / ↑n ^ s) (HurwitzZeta.completedSinZeta (↑a) s)

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

theorem HurwitzZeta.hasSum_int_completedHurwitzZetaOdd (a : ℝ) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (n : ℤ) => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (HurwitzZeta.completedHurwitzZetaOdd (↑a) s)

Formula for completedHurwitzZetaOdd as a Dirichlet series in the convergence range.

Non-completed zeta functions

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

The odd part of the Hurwitz zeta function, i.e. the meromorphic function of s which agrees with 1 / 2 * ∑' (n : ℤ), sign (n + a) / |n + a| ^ s for 1 < re s

Equations

• HurwitzZeta.hurwitzZetaOdd a s = HurwitzZeta.completedHurwitzZetaOdd a s / (s + 1).Gammaℝ

theorem HurwitzZeta.hurwitzZetaOdd_neg (a : UnitAddCircle) (s : ℂ) : HurwitzZeta.hurwitzZetaOdd (-a) s = -HurwitzZeta.hurwitzZetaOdd a s

theorem HurwitzZeta.differentiable_hurwitzZetaOdd (a : UnitAddCircle) : Differentiable ℂ (HurwitzZeta.hurwitzZetaOdd a)

The odd Hurwitz zeta function is differentiable everywhere.

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

The sine zeta function, i.e. the meromorphic function of s which agrees with ∑' (n : ℕ), sin (2 * π * a * n) / n ^ s for 1 < re s.

Equations

• HurwitzZeta.sinZeta a s = HurwitzZeta.completedSinZeta a s / (s + 1).Gammaℝ

theorem HurwitzZeta.sinZeta_neg (a : UnitAddCircle) (s : ℂ) : HurwitzZeta.sinZeta (-a) s = -HurwitzZeta.sinZeta a s

theorem HurwitzZeta.differentiableAt_sinZeta (a : UnitAddCircle) : Differentiable ℂ (HurwitzZeta.sinZeta a)

The sine zeta function is differentiable everywhere.

theorem HurwitzZeta.hasSum_int_hurwitzZetaOdd (a : ℝ) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (n : ℤ) => ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (HurwitzZeta.hurwitzZetaOdd (↑a) s)

Formula for hurwitzZetaOdd as a Dirichlet series in the convergence range (sum over ℤ).

theorem HurwitzZeta.hasSum_nat_hurwitzZetaOdd (a : ℝ) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (n : ℕ) => (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2) (HurwitzZeta.hurwitzZetaOdd (↑a) s)

Formula for hurwitzZetaOdd as a Dirichlet series in the convergence range, with sum over ℕ (version with absolute values)

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

Formula for hurwitzZetaOdd as a Dirichlet series in the convergence range, with sum over ℕ (version without absolute values, assuming a ∈ Icc 0 1)

theorem HurwitzZeta.hasSum_int_sinZeta (a : ℝ) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (n : ℤ) => -Complex.I * ↑n.sign * Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2) (HurwitzZeta.sinZeta (↑a) s)

Formula for sinZeta as a Dirichlet series in the convergence range, with sum over ℤ.

theorem HurwitzZeta.hasSum_nat_sinZeta (a : ℝ) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (n : ℕ) => ↑(Real.sin (2 * Real.pi * a * ↑n)) / ↑n ^ s) (HurwitzZeta.sinZeta (↑a) s)

Formula for sinZeta as a Dirichlet series in the convergence range, with sum over ℕ.

theorem HurwitzZeta.LSeriesHasSum_sin (a : ℝ) {s : ℂ} (hs : 1 < s.re) : LSeriesHasSum (fun (x : ℕ) => ↑(Real.sin (2 * Real.pi * a * ↑x))) s (HurwitzZeta.sinZeta (↑a) s)

Reformulation of hasSum_nat_sinZeta using LSeriesHasSum.

theorem HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat_sub_one (a : UnitAddCircle) (n : ℕ) : HurwitzZeta.hurwitzZetaOdd a (-2 * ↑n - 1) = 0

The trivial zeroes of the odd Hurwitz zeta function.

theorem HurwitzZeta.sinZeta_neg_two_mul_nat_sub_one (a : UnitAddCircle) (n : ℕ) : HurwitzZeta.sinZeta a (-2 * ↑n - 1) = 0

The trivial zeroes of the sine zeta function.

theorem HurwitzZeta.hurwitzZetaOdd_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) : HurwitzZeta.hurwitzZetaOdd a (1 - s) = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.sin (↑Real.pi * s / 2) * HurwitzZeta.sinZeta a s

If s is not in -ℕ, then hurwitzZetaOdd a (1 - s) is an explicit multiple of sinZeta s.

theorem HurwitzZeta.sinZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) : HurwitzZeta.sinZeta a (1 - s) = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.sin (↑Real.pi * s / 2) * HurwitzZeta.hurwitzZetaOdd a s

If s is not in -ℕ, then sinZeta a (1 - s) is an explicit multiple of hurwitzZetaOdd s.