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:

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

and

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

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 completed versions of these functions with nicer functional equations (satisfying completedHurwitzZetaEven a s = Gammaℝ s * hurwitzZetaEven a s, and similarly for cosZeta); and 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

• hurwitzZetaEven and cosZeta: the zeta functions
• completedHurwitzZetaEven and completedCosZeta: completed variants
• differentiableAt_hurwitzZetaEven and differentiableAt_cosZeta: differentiability away from s = 1
• completedHurwitzZetaEven_one_sub: the functional equation completedHurwitzZetaEven a (1 - s) = completedCosZeta a s
• hasSum_int_hurwitzZetaEven and hasSum_nat_cosZeta: relation between the zeta functions and the corresponding Dirichlet series for 1 < re s.

Definitions and elementary properties of kernels

@[irreducible]

def HurwitzZeta.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

• HurwitzZeta.evenKernel a x = ⋯.lift a

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

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

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

@[irreducible]

def HurwitzZeta.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

• HurwitzZeta.cosKernel a x = ⋯.lift a

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

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

theorem HurwitzZeta.evenKernel_eq_cosKernel_of_zero : HurwitzZeta.evenKernel 0 = HurwitzZeta.cosKernel 0

For a = 0, both kernels agree.

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

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

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

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

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

Formulae for the kernels as sums

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

theorem HurwitzZeta.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))) ↑(HurwitzZeta.cosKernel (↑a) t)

theorem HurwitzZeta.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)) (HurwitzZeta.evenKernel (↑a) t - if ↑a = 0 then 1 else 0)

Modified version of hasSum_int_evenKernel omitting the constant term at ∞.

theorem HurwitzZeta.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))) (↑(HurwitzZeta.cosKernel (↑a) t) - 1)

theorem HurwitzZeta.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)) (HurwitzZeta.cosKernel (↑a) t - 1)

Asymptotics of the kernels as t → ∞

theorem HurwitzZeta.isBigO_atTop_evenKernel_sub (a : UnitAddCircle) : ∃ (p : ℝ), 0 < p ∧ (fun (x : ℝ) => HurwitzZeta.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 HurwitzZeta.isBigO_atTop_cosKernel_sub (a : UnitAddCircle) : ∃ (p : ℝ), 0 < p ∧ (fun (x : ℝ) => HurwitzZeta.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 HurwitzZeta.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 HurwitzZeta.hurwitzEvenFEPair_zero_symm : (HurwitzZeta.hurwitzEvenFEPair 0).symm = HurwitzZeta.hurwitzEvenFEPair 0

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

Definition of the completed even Hurwitz zeta function

def HurwitzZeta.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

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

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

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

Equations

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

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

def HurwitzZeta.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

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

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

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

Equations

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

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

Parity and functional equations

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

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

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

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

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

Functional equation for the even Hurwitz zeta function.

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

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

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

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

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

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

Differentiability and residues

theorem HurwitzZeta.differentiableAt_completedHurwitzZetaEven (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 0 ∨ a ≠ 0) (hs' : s ≠ 1) : DifferentiableAt ℂ (HurwitzZeta.completedHurwitzZetaEven a) s

The even Hurwitz completed zeta is differentiable away from s = 0 and s = 1 (and also at s = 0 if a ≠ 0)

theorem HurwitzZeta.differentiable_completedHurwitzZetaEven₀ (a : UnitAddCircle) : Differentiable ℂ (HurwitzZeta.completedHurwitzZetaEven₀ a)

theorem HurwitzZeta.differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven (a : UnitAddCircle) (b : UnitAddCircle) : DifferentiableAt ℂ (fun (s : ℂ) => HurwitzZeta.completedHurwitzZetaEven a s - HurwitzZeta.completedHurwitzZetaEven b s) 1

The difference of two completed even Hurwitz zeta functions is differentiable at s = 1.

theorem HurwitzZeta.differentiableAt_completedCosZeta (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 0) (hs' : s ≠ 1 ∨ a ≠ 0) : DifferentiableAt ℂ (HurwitzZeta.completedCosZeta a) s

theorem HurwitzZeta.differentiable_completedCosZeta₀ (a : UnitAddCircle) : Differentiable ℂ (HurwitzZeta.completedCosZeta₀ a)

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

The residue of completedHurwitzZetaEven a s at s = 1 is equal to 1.

theorem HurwitzZeta.completedHurwitzZetaEven_residue_zero (a : UnitAddCircle) : Filter.Tendsto (fun (s : ℂ) => s * HurwitzZeta.completedHurwitzZetaEven a s) (nhdsWithin 0 {0}ᶜ) (nhds (if a = 0 then -1 else 0))

The residue of completedHurwitzZetaEven a s at s = 0 is equal to -1 if a = 0, and 0 otherwise.

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

Relation to the Dirichlet series for 1 < re s

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

theorem HurwitzZeta.hasSum_nat_completedCosZeta (a : ℝ) {s : ℂ} (hs : 1 < s.re) : HasSum (fun (n : ℕ) => if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * Real.pi * a * ↑n)) / ↑n ^ s) (HurwitzZeta.completedCosZeta (↑a) s)

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

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

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

The un-completed even Hurwitz zeta

theorem HurwitzZeta.differentiableAt_update_of_residue {Λ : ℂ → ℂ} (hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s) {L : ℂ} (h_lim : Filter.Tendsto (fun (s : ℂ) => s * Λ s) (nhdsWithin 0 {0}ᶜ) (nhds L)) (s : ℂ) (hs' : s ≠ 1) : DifferentiableAt ℂ (Function.update (fun (s : ℂ) => Λ s / s.Gammaℝ) 0 (L / 2)) s

Technical lemma which will give us differentiability of Hurwitz zeta at s = 0.

noncomputable def HurwitzZeta.hurwitzZetaEven (a : UnitAddCircle) (a : ℂ) : ℂ

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

Equations

• HurwitzZeta.hurwitzZetaEven a = Function.update (fun (s : ℂ) => HurwitzZeta.completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0)

theorem HurwitzZeta.hurwitzZetaEven_def_of_ne_or_ne {a : UnitAddCircle} {s : ℂ} (h : a ≠ 0 ∨ s ≠ 0) : HurwitzZeta.hurwitzZetaEven a s = HurwitzZeta.completedHurwitzZetaEven a s / s.Gammaℝ

theorem HurwitzZeta.hurwitzZetaEven_apply_zero (a : UnitAddCircle) : HurwitzZeta.hurwitzZetaEven a 0 = if a = 0 then -1 / 2 else 0

theorem HurwitzZeta.hurwitzZetaEven_neg (a : UnitAddCircle) (s : ℂ) : HurwitzZeta.hurwitzZetaEven (-a) s = HurwitzZeta.hurwitzZetaEven a s

theorem HurwitzZeta.hurwitzZetaEven_neg_two_mul_nat_add_one (a : UnitAddCircle) (n : ℕ) : HurwitzZeta.hurwitzZetaEven a (-2 * (↑n + 1)) = 0

The trivial zeroes of the even Hurwitz zeta function.

theorem HurwitzZeta.differentiableAt_hurwitzZetaEven (a : UnitAddCircle) {s : ℂ} (hs' : s ≠ 1) : DifferentiableAt ℂ (HurwitzZeta.hurwitzZetaEven a) s

The Hurwitz zeta function is differentiable everywhere except at s = 1. This is true even in the delicate case a = 0 and s = 0 (where the completed zeta has a pole, but this is cancelled out by the Gamma factor).

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

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

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

Expression for hurwitzZetaEven a 1 as a limit. (Mathematically hurwitzZetaEven 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_hurwitzZetaEven_sub_hurwitzZetaEven (a : UnitAddCircle) (b : UnitAddCircle) : Differentiable ℂ fun (s : ℂ) => HurwitzZeta.hurwitzZetaEven a s - HurwitzZeta.hurwitzZetaEven b s

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

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

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

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

theorem HurwitzZeta.hasSum_nat_hurwitzZetaEven_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.hurwitzZetaEven (↑a) s)

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

The un-completed cosine zeta

noncomputable def HurwitzZeta.cosZeta (a : UnitAddCircle) (a : ℂ) : ℂ

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

Equations

• HurwitzZeta.cosZeta a = Function.update (fun (s : ℂ) => HurwitzZeta.completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2)

theorem HurwitzZeta.cosZeta_apply_zero (a : UnitAddCircle) : HurwitzZeta.cosZeta a 0 = -1 / 2

theorem HurwitzZeta.cosZeta_neg (a : UnitAddCircle) (s : ℂ) : HurwitzZeta.cosZeta (-a) s = HurwitzZeta.cosZeta a s

theorem HurwitzZeta.cosZeta_neg_two_mul_nat_add_one (a : UnitAddCircle) (n : ℕ) : HurwitzZeta.cosZeta a (-2 * (↑n + 1)) = 0

The trivial zeroes of the cosine zeta function.

theorem HurwitzZeta.differentiableAt_cosZeta (a : UnitAddCircle) {s : ℂ} (hs' : s ≠ 1 ∨ a ≠ 0) : DifferentiableAt ℂ (HurwitzZeta.cosZeta a) s

The cosine zeta function is differentiable everywhere, except at s = 1 if a = 0.

theorem HurwitzZeta.differentiable_cosZeta_of_ne_zero {a : UnitAddCircle} (ha : a ≠ 0) : Differentiable ℂ (HurwitzZeta.cosZeta a)

If a ≠ 0 then the cosine zeta function is entire.

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

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

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

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

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

Reformulation of hasSum_nat_cosZeta using LSeriesHasSum.

Functional equations for the un-completed zetas

theorem HurwitzZeta.hurwitzZetaEven_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) (hs' : a ≠ 0 ∨ s ≠ 1) : HurwitzZeta.hurwitzZetaEven a (1 - s) = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.cos (↑Real.pi * s / 2) * HurwitzZeta.cosZeta a s

If s is not in -ℕ, and either a ≠ 0 or s ≠ 1, then hurwitzZetaEven a (1 - s) is an explicit multiple of cosZeta s.

theorem HurwitzZeta.cosZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ 1 - ↑n) : HurwitzZeta.cosZeta a (1 - s) = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.cos (↑Real.pi * s / 2) * HurwitzZeta.hurwitzZetaEven a s

If s is not of the form 1 - n for n ∈ ℕ, then cosZeta a (1 - s) is an explicit multiple of hurwitzZetaEven s.