Documentation

Mathlib.NumberTheory.LSeries.HurwitzZeta

The Hurwitz zeta function #

This file gives the definition and properties of the following two functions:

Main definitions and results #

The Hurwitz zeta function #

noncomputable def HurwitzZeta.hurwitzZeta (a : UnitAddCircle) (s : ) :

The Hurwitz zeta function, which is the meromorphic continuation of ∑ (n : ℕ), 1 / (n + a) ^ s if 0 ≤ a ≤ 1. See hasSum_hurwitzZeta_of_one_lt_re for the relation to the Dirichlet series in the convergence range.

Equations
Instances For

    The Hurwitz zeta function is differentiable away from s = 1.

    theorem HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re {a : } (ha : a Set.Icc 0 1) {s : } (hs : 1 < s.re) :
    HasSum (fun (n : ) => 1 / (n + a) ^ s) (HurwitzZeta.hurwitzZeta (↑a) s)

    Formula for hurwitzZeta s as a Dirichlet series in the convergence range. We restrict to a ∈ Icc 0 1 to simplify the statement.

    The residue of the Hurwitz zeta function at s = 1 is 1.

    Expression for hurwitzZeta a 1 as a limit. (Mathematically hurwitzZeta a 1 is undefined, but our construction assigns some value to it; this lemma is mostly of interest for determining what that value is).

    The difference of two Hurwitz zeta functions is differentiable everywhere.

    The exponential zeta function #

    noncomputable def HurwitzZeta.expZeta (a : UnitAddCircle) (s : ) :

    Meromorphic continuation of the series ∑' (n : ℕ), exp (2 * π * I * a * n) / n ^ s. See hasSum_expZeta_of_one_lt_re for the relation to the Dirichlet series.

    Equations
    Instances For
      theorem HurwitzZeta.hasSum_expZeta_of_one_lt_re (a : ) {s : } (hs : 1 < s.re) :
      HasSum (fun (n : ) => Complex.exp (2 * Real.pi * Complex.I * a * n) / n ^ s) (HurwitzZeta.expZeta (↑a) s)

      If a ≠ 0 then the exponential zeta function is analytic everywhere.

      theorem HurwitzZeta.LSeriesHasSum_exp (a : ) {s : } (hs : 1 < s.re) :
      LSeriesHasSum (fun (x : ) => Complex.exp (2 * Real.pi * Complex.I * a * x)) s (HurwitzZeta.expZeta (↑a) s)

      Reformulation of hasSum_expZeta_of_one_lt_re using LSeriesHasSum.

      The functional equation #

      Functional equation for the exponential zeta function.