Documentation

Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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 #

Definitions and elementary properties of kernels #

@[irreducible]

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
Instances For
    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)

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

    @[irreducible]

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

    Equations
    Instances For
      theorem HurwitzZeta.cosKernel_def (a : ) (x : ) :
      (HurwitzZeta.cosKernel (↑a) x) = jacobiTheta₂ (↑a) (Complex.I * 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 #

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

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

        Definition of the completed even Hurwitz zeta function #

        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
        Instances For

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

          Equations
          Instances For

            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
            Instances For

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

              Equations
              Instances For

                Parity and functional equations #

                Functional equation for the even Hurwitz zeta function.

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

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

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

                Differentiability and residues #

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

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

                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 0s 1DifferentiableAt Λ 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
                Instances For

                  The trivial zeroes of the even Hurwitz zeta function.

                  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).

                  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.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
                  Instances For

                    The trivial zeroes of the cosine zeta function.

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

                    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) :

                    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) :

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