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 from s = 0 and s = 1.
• differentiableAt_riemannZeta : the function ζ(s) is differentiable away from s = 1.
• zeta_eq_tsum_one_div_nat_add_one_cpow : for 1 < re s, we have ζ(s) = ∑' (n : ℕ), 1 / (n + 1) ^ s.
• completedRiemannZeta₀_one_sub, completedRiemannZeta_one_sub, and riemannZeta_one_sub : functional equation relating values at s and 1 - s

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

Outline of proofs:

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

Definition of the completed Riemann zeta

def completedRiemannZeta₀ (s : ℂ) : ℂ

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

Equations

• completedRiemannZeta₀ s = HurwitzZeta.completedHurwitzZetaEven₀ 0 s

def completedRiemannZeta (s : ℂ) : ℂ

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

Equations

• completedRiemannZeta s = HurwitzZeta.completedHurwitzZetaEven 0 s

theorem HurwitzZeta.completedHurwitzZetaEven_zero (s : ℂ) : completedHurwitzZetaEven 0 s = completedRiemannZeta s

theorem HurwitzZeta.completedHurwitzZetaEven₀_zero (s : ℂ) : completedHurwitzZetaEven₀ 0 s = completedRiemannZeta₀ s

theorem HurwitzZeta.completedCosZeta_zero (s : ℂ) : completedCosZeta 0 s = completedRiemannZeta s

theorem HurwitzZeta.completedCosZeta₀_zero (s : ℂ) : completedCosZeta₀ 0 s = completedRiemannZeta₀ s

theorem completedRiemannZeta_eq (s : ℂ) : completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)

theorem differentiable_completedZeta₀ : Differentiable ℂ completedRiemannZeta₀

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

theorem differentiableAt_completedZeta {s : ℂ} (hs : s ≠ 0) (hs' : s ≠ 1) : DifferentiableAt ℂ completedRiemannZeta s

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

theorem completedRiemannZeta₀_one_sub (s : ℂ) : completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s

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

theorem completedRiemannZeta_one_sub (s : ℂ) : completedRiemannZeta (1 - s) = completedRiemannZeta s

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

theorem completedRiemannZeta_residue_one : Filter.Tendsto (fun (s : ℂ) => (s - 1) * completedRiemannZeta s) (nhdsWithin 1 {1}ᶜ) (nhds 1)

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

• riemannZeta = HurwitzZeta.hurwitzZetaEven 0

theorem HurwitzZeta.hurwitzZetaEven_zero : hurwitzZetaEven 0 = riemannZeta

theorem HurwitzZeta.cosZeta_zero : cosZeta 0 = riemannZeta

theorem HurwitzZeta.hurwitzZeta_zero : hurwitzZeta 0 = riemannZeta

theorem HurwitzZeta.expZeta_zero : expZeta 0 = riemannZeta

theorem differentiableAt_riemannZeta {s : ℂ} (hs' : s ≠ 1) : DifferentiableAt ℂ riemannZeta s

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

theorem riemannZeta_zero : riemannZeta 0 = -1 / 2

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

theorem riemannZeta_def_of_ne_zero {s : ℂ} (hs : s ≠ 0) : riemannZeta s = completedRiemannZeta s / s.Gammaℝ

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) : riemannZeta (1 - s) = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.cos (↑Real.pi * s / 2) * riemannZeta s

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

def RiemannHypothesis : Prop

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

Equations

• RiemannHypothesis = ∀ (s : ℂ), riemannZeta s = 0 → (¬∃ (n : ℕ), s = -2 * (↑n + 1)) → s ≠ 1 → s.re = 1 / 2

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 two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even {k : ℕ} (hk : 2 ≤ k) (hk2 : Even k) : 2 * riemannZeta ↑k = ∑' (n : ℤ), (↑n ^ k)⁻¹

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.

theorem tendsto_sub_mul_tsum_nat_cpow : Filter.Tendsto (fun (s : ℂ) => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) (nhdsWithin 1 {s : ℂ | 1 < s.re}) (nhds 1)

The residue of ζ(s) at s = 1 is equal to 1, expressed using tsum.

theorem tendsto_sub_mul_tsum_nat_rpow : Filter.Tendsto (fun (s : ℝ) => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) (nhdsWithin 1 (Set.Ioi 1)) (nhds 1)

The residue of ζ(s) at s = 1 is equal to 1 expressed using tsum and for a real variable.