Definition of the Riemann zeta function #
Main definitions: #
riemannZeta
: the Riemann zeta functionζ : ℂ → ℂ
.completedRiemannZeta
: the completed zeta functionΛ : ℂ → ℂ
, which satisfiesΛ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s)
(away from the poles ofΓ(s / 2)
).completedRiemannZeta₀
: the entire functionΛ₀
satisfyingΛ₀(s) = Λ(s) + 1 / (s - 1) - 1 / s
wherever the RHS is defined.
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: #
differentiable_completedZeta₀
: the functionΛ₀(s)
is entire.differentiableAt_completedZeta
: the functionΛ(s)
is differentiable away froms = 0
ands = 1
.differentiableAt_riemannZeta
: the functionζ(s)
is differentiable away froms = 1
.zeta_eq_tsum_one_div_nat_add_one_cpow
: for1 < re s
, we haveζ(s) = ∑' (n : ℕ), 1 / (n + 1) ^ s
.completedRiemannZeta₀_one_sub
,completedRiemannZeta_one_sub
, andriemannZeta_one_sub
: functional equation relating values ats
and1 - s
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 #
The Riemann zeta function ζ(s)
.
Equations
Instances For
The Riemann zeta function is differentiable away from s = 1
.
The trivial zeroes of the zeta function.
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 #
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
.)
Alternate formulation of zeta_eq_tsum_one_div_nat_cpow
with a + 1
(to avoid relying
on mathlib's conventions for 0 ^ s
).
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
.
The residue of ζ(s)
at s = 1
is equal to 1.
Alias of completedRiemannZeta₀
.
The completed Riemann zeta function with its poles removed, Λ(s) + 1 / s - 1 / (s - 1)
.
Equations
Instances For
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
Alias of completedRiemannZeta₀_one_sub
.
Riemann zeta functional equation, formulated for Λ₀
: for any complex s
we have
Λ₀(1 - s) = Λ₀ s
.
Alias of completedRiemannZeta_one_sub
.
Riemann zeta functional equation, formulated for Λ
: for any complex s
we have
Λ (1 - s) = Λ s
.
Alias of completedRiemannZeta_residue_one
.
The residue of Λ(s)
at s = 1
is equal to 1
.