Documentation

Mathlib.NumberTheory.LSeries.RiemannZeta

Definition of the Riemann zeta function #

Main definitions: #

Note that mathematically ζ(s) is undefined at s = 1, while Λ(s) is undefined at both s = 0 and s = 1. Our construction assigns some values at these points; exact formulae involving the Euler-Mascheroni constant will follow in a subsequent PR.

Main results: #

For special-value formulae expressing ζ (2 * k) and ζ (1 - 2 * k) in terms of Bernoulli numbers see Mathlib.NumberTheory.LSeries.HurwitzZetaValues. For computation of the constant term as s → 1, see Mathlib.NumberTheory.Harmonic.ZetaAsymp.

Outline of proofs: #

These results are mostly special cases of more general results for even Hurwitz zeta functions proved in Mathlib.NumberTheory.LSeries.HurwitzZetaEven.

Definition of the completed Riemann zeta #

The completed Riemann zeta function with its poles removed, Λ(s) + 1 / s - 1 / (s - 1).

Equations
Instances For

    The completed Riemann zeta function, Λ(s), which satisfies Λ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s) (up to a minor correction at s = 0).

    Equations
    Instances For

      The modified completed Riemann zeta function Λ(s) + 1 / s + 1 / (1 - s) is entire.

      The completed Riemann zeta function Λ(s) is differentiable away from s = 0 and s = 1.

      Riemann zeta functional equation, formulated for Λ₀: for any complex s we have Λ₀(1 - s) = Λ₀ s.

      Riemann zeta functional equation, formulated for Λ: for any complex s we have Λ (1 - s) = Λ s.

      The residue of Λ(s) at s = 1 is equal to 1.

      The un-completed Riemann zeta function #

      def riemannZeta (a : ) :

      The Riemann zeta function ζ(s).

      Equations
      Instances For

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

        theorem riemannZeta_zero :
        riemannZeta 0 = -1 / 2

        We have ζ(0) = -1 / 2.

        theorem riemannZeta_neg_two_mul_nat_add_one (n : ) :
        riemannZeta (-2 * (n + 1)) = 0

        The trivial zeroes of the zeta function.

        theorem riemannZeta_one_sub {s : } (hs : ∀ (n : ), s -n) (hs' : s 1) :

        Riemann zeta functional equation, formulated for ζ: if 1 - s ∉ ℕ, then we have ζ (1 - s) = 2 ^ (1 - s) * π ^ (-s) * Γ s * sin (π * (1 - s) / 2) * ζ s.

        A formal statement of the Riemann hypothesis – constructing a term of this type is worth a million dollars.

        Equations
        Instances For

          Relating the Mellin transform to the Dirichlet series #

          theorem completedZeta_eq_tsum_of_one_lt_re {s : } (hs : 1 < s.re) :
          completedRiemannZeta s = Real.pi ^ (-s / 2) * Complex.Gamma (s / 2) * ∑' (n : ), 1 / n ^ s
          theorem zeta_eq_tsum_one_div_nat_cpow {s : } (hs : 1 < s.re) :
          riemannZeta s = ∑' (n : ), 1 / n ^ s

          The Riemann zeta function agrees with the naive Dirichlet-series definition when the latter converges. (Note that this is false without the assumption: when re s ≤ 1 the sum is divergent, and we use a different definition to obtain the analytic continuation to all s.)

          theorem zeta_eq_tsum_one_div_nat_add_one_cpow {s : } (hs : 1 < s.re) :
          riemannZeta s = ∑' (n : ), 1 / (n + 1) ^ s

          Alternate formulation of zeta_eq_tsum_one_div_nat_cpow with a + 1 (to avoid relying on mathlib's conventions for 0 ^ s).

          theorem zeta_nat_eq_tsum_of_gt_one {k : } (hk : 1 < k) :
          riemannZeta k = ∑' (n : ), 1 / n ^ k

          Special case of zeta_eq_tsum_one_div_nat_cpow when the argument is in , so the power function can be expressed using naïve pow rather than cpow.

          theorem riemannZeta_residue_one :
          Filter.Tendsto (fun (s : ) => (s - 1) * riemannZeta s) (nhdsWithin 1 {1}) (nhds 1)

          The residue of ζ(s) at s = 1 is equal to 1.

          @[deprecated completedRiemannZeta₀]

          Alias of completedRiemannZeta₀.


          The completed Riemann zeta function with its poles removed, Λ(s) + 1 / s - 1 / (s - 1).

          Equations
          Instances For
            @[deprecated completedRiemannZeta]

            Alias of completedRiemannZeta.


            The completed Riemann zeta function, Λ(s), which satisfies Λ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s) (up to a minor correction at s = 0).

            Equations
            Instances For
              @[deprecated completedRiemannZeta₀_one_sub]

              Alias of completedRiemannZeta₀_one_sub.


              Riemann zeta functional equation, formulated for Λ₀: for any complex s we have Λ₀(1 - s) = Λ₀ s.

              @[deprecated completedRiemannZeta_one_sub]

              Alias of completedRiemannZeta_one_sub.


              Riemann zeta functional equation, formulated for Λ: for any complex s we have Λ (1 - s) = Λ s.

              @[deprecated completedRiemannZeta_residue_one]

              Alias of completedRiemannZeta_residue_one.


              The residue of Λ(s) at s = 1 is equal to 1.