Documentation

Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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 #

Definitions and elementary properties of kernels #

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

Equations
Instances For
    @[irreducible]

    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
    Instances For
      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))
      @[irreducible]

      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
      Instances For
        theorem HurwitzZeta.sinKernel_def (a : ) (x : ) :
        (HurwitzZeta.sinKernel (↑a) x) = jacobiTheta₂' (↑a) (Complex.I * x) / (-2 * Real.pi)

        The odd kernel is continuous on Ioi 0.

        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 #

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

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

          Definition of the completed odd Hurwitz zeta function #

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

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

              Parity and functional equations #

              Functional equation for the odd Hurwitz zeta function.

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

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

                  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.

                  The trivial zeroes of the odd Hurwitz zeta function.

                  The trivial zeroes of the sine zeta function.

                  theorem HurwitzZeta.hurwitzZetaOdd_one_sub (a : UnitAddCircle) {s : } (hs : ∀ (n : ), s -n) :

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

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